Ltac_plugin.TacinternGlobalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr
type glob_sign = Genintern.glob_sign = {ltacvars : Names.Id.Set.t; |
genv : Environ.env; |
extra : Genintern.Store.t; |
intern_sign : Genintern.intern_variable_status; |
strict_check : bool; |
}val make_empty_glob_sign : strict:bool -> glob_signbuild an empty glob_sign using Global.env() as environment; strict_check if true
Main globalization functions
val glob_tactic : Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_exprval glob_tactic_env : Names.Id.t list -> Environ.env -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_exprLow-level variants
val intern_pure_tactic : glob_sign -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_exprval intern_tactic_or_tacarg : glob_sign -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_exprval intern_constr : glob_sign -> Constrexpr.constr_expr -> Genintern.glob_constr_and_exprval 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.bindingsval intern_hyp : glob_sign -> Names.lident -> Names.lidentAdds a globalization function for extra generic arguments
val intern_genarg : glob_sign -> Genarg.raw_generic_argument -> Genarg.glob_generic_argumentReduction expressions
val intern_red_expr : glob_sign -> Genredexpr.raw_red_expr -> Genredexpr.glob_red_exprval intern_strategy : glob_sign -> Tacexpr.raw_strategy -> Tacexpr.glob_strategy