Module Ltac_plugin.Tacintern

type glob_sign = Genintern.glob_sign = {
ltacvars : Names.Id.Set.t;
genv : Environ.env;
extra : Genintern.Store.t;
intern_sign : Genintern.intern_variable_status;
}
val make_empty_glob_sign : unit -> glob_sign

build an empty glob_sign using Global.env() as environment

val glob_tactic : Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr
val glob_tactic_env : Names.Id.t list -> Environ.env -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr
val intern_pure_tactic : glob_sign -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr
val intern_tactic_or_tacarg : glob_sign -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr
val intern_constr : glob_sign -> Constrexpr.constr_expr -> Genintern.glob_constr_and_expr
val intern_constr_with_bindings : glob_sign -> (Constrexpr.constr_expr * Constrexpr.constr_expr Tactypes.bindings) -> Genintern.glob_constr_and_expr * Genintern.glob_constr_and_expr Tactypes.bindings
val intern_hyp : glob_sign -> Names.lident -> Names.lident
val intern_genarg : glob_sign -> Genarg.raw_generic_argument -> Genarg.glob_generic_argument
val intern_red_expr : glob_sign -> Tacexpr.raw_red_expr -> Tacexpr.glob_red_expr
val dump_glob_red_expr : Tacexpr.raw_red_expr -> unit
val strict_check : bool Stdlib.ref