Intern (rocq-runtime.Redexpr.Intern)

type ('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 ->
  raw_red_expr ->
  ('a, 'b, 'c, int Locus.or_var, Genarg.glevel user_red_expr)
    Genredexpr.red_expr_gen

val from_env : 
  Environ.env ->
  (Glob_term.glob_constr, Evaluable.t, Glob_term.glob_constr) intern_env