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 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 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