ConstrexternSourceTranslation 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_cases_pattern :
flags:PrintingFlags.Extern.t ->
Names.Id.Set.t ->
'a Glob_term.cases_pattern_g ->
Constrexpr.cases_pattern_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_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.qualidProbably shouldn't be used