Module `Constrextern`

Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing

val extern_cases_pattern : Names.Id.Set.t -> 'a Glob_term.cases_pattern_g -> Constrexpr.cases_pattern_expr
val extern_glob_constr : Names.Id.Set.t -> 'a Glob_term.glob_constr_g -> Constrexpr.constr_expr
val extern_glob_type : Names.Id.Set.t -> 'a Glob_term.glob_constr_g -> Constrexpr.constr_expr
val extern_constr_pattern : Termops.names_context -> Evd.evar_map -> Pattern.constr_pattern -> Constrexpr.constr_expr
val extern_closed_glob : ?⁠lax:bool -> bool -> Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Constrexpr.constr_expr

val extern_constr : ?⁠lax:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_expr
val extern_constr_in_scope : bool -> Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_expr
val extern_reference : ?⁠loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
val extern_type : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Constrexpr.constr_expr
val extern_sort : Evd.evar_map -> Sorts.t -> Glob_term.glob_sort
val extern_rel_context : EConstr.constr option -> Environ.env -> Evd.evar_map -> EConstr.rel_context -> Constrexpr.local_binder_expr list
val print_implicits : bool Stdlib.ref: Printing options

val print_implicits_defensive : bool Stdlib.ref
val print_arguments : bool Stdlib.ref
val print_evar_arguments : bool Stdlib.ref
val print_coercions : bool Stdlib.ref
val print_universes : bool Stdlib.ref
val print_no_symbol : bool Stdlib.ref
val print_projections : bool Stdlib.ref
val set_extern_reference : (?⁠loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid) -> unit: Customization of the global_reference printer

val get_extern_reference : unit -> ?⁠loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid

val with_universes : ('a -> 'b) -> 'a -> 'b: This forces printing universe names of Type{.}

val without_symbols : ('a -> 'b) -> 'a -> 'b: This suppresses printing of primitive tokens and notations

val without_specific_symbols : Notation.interp_rule list -> ('a -> 'b) -> 'a -> 'b: This suppresses printing of specific notations only

val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b: This prints metas as anonymous holes

val toggle_scope_printing : scope:Notation_term.scope_name -> activate:bool -> unit: Fine-grained activation and deactivation of notation printing.

val toggle_notation_printing : ?⁠scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit