Redexpr.Interntype ('constr, 'ref, 'pat) intern_env = {strict_check : bool; |
local_ref : Libnames.qualid -> 'ref option; |
global_ref : ?short:Names.lident -> Evaluable.t -> 'ref; |
intern_constr : Constrexpr.constr_expr -> 'constr; |
ltac_sign : Constrintern.ltac_sign; |
intern_pattern : Constrexpr.constr_expr -> 'pat; |
pattern_of_glob : Glob_term.glob_constr -> 'pat; |
}val intern_red_expr : ('a, 'b, 'c) intern_env -> Genredexpr.raw_red_expr -> ('a, 'b, 'c, int Locus.or_var) Genredexpr.red_expr_genval from_env : Environ.env -> (Glob_term.glob_constr, Evaluable.t, Glob_term.glob_constr) intern_env