Module Gentactic

Generic tactic expressions. Internally implemented using Genarg.

type raw_generic_tactic
type glob_generic_tactic

The genarg must have registrations for all the following APIs.

The genarg must have registrations for all the following APIs except those operating at the "raw" level.

val intern : ?strict:bool -> Environ.env -> ?ltacvars:Names.Id.Set.t -> raw_generic_tactic -> glob_generic_tactic

strict is default true

For serlib