ConstrexternTranslation of pattern, cases pattern, glob_constr and term into syntax trees for printing
type extern_env = {vars : Names.Id.Set.t; |
uvars : UnivNames.universe_binders; |
flags : PrintingFlags.Extern.t; |
}val extern_env : flags:PrintingFlags.Extern.t -> Environ.env -> Evd.evar_map -> extern_envval extern_cases_pattern : flags:PrintingFlags.Extern.t -> Names.Id.Set.t -> 'a Glob_term.cases_pattern_g -> Constrexpr.cases_pattern_exprval extern_glob_constr : extern_env -> 'a Glob_term.glob_constr_g -> Constrexpr.constr_exprval extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a Glob_term.glob_constr_g -> Constrexpr.constr_exprval extern_constr_pattern : flags:PrintingFlags.Extern.t -> Termops.names_context -> Evd.evar_map -> Pattern.constr_pattern -> Constrexpr.constr_exprval extern_uninstantiated_pattern : flags:PrintingFlags.Extern.t -> Termops.names_context -> Evd.evar_map -> Pattern.uninstantiated_pattern -> Constrexpr.constr_exprval extern_closed_glob : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> flags:PrintingFlags.t
-> Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Constrexpr.constr_exprIf b=true in extern_constr b env c then the variables in the first level of quantification clashing with the variables in env are renamed. ~lax is for debug printing, when the constr might not be well typed in env, sigma
val extern_constr : ?inctx:bool -> ?scope:Notation_term.scope_name -> flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_exprval extern_constr_in_scope : ?inctx:bool -> Notation_term.scope_name -> flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_exprval extern_reference : ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualidval extern_type : ?goal_concl_style:bool -> flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Constrexpr.constr_exprval extern_sort : universes:bool -> qualities:bool -> Evd.evar_map -> Sorts.t -> Constrexpr.sort_exprval extern_rel_context : flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> EConstr.rel_context -> Constrexpr.local_binder_expr listval set_extern_reference : (?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid) -> unitCustomization of the global_reference printer
val get_extern_reference : unit -> ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualidval empty_extern_env : flags:PrintingFlags.Extern.t -> extern_envProbably shouldn't be used