package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ConstrexternSource

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

Sourceval extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Constrexpr.constr_expr

If 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

Sourceval extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_expr
Sourceval extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_expr
Sourceval extern_reference : ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
Sourceval extern_type : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Constrexpr.constr_expr
Sourceval print_implicits : bool ref

Printing options

Sourceval print_implicits_defensive : bool ref
Sourceval print_arguments : bool ref
Sourceval print_evar_arguments : bool ref
Sourceval print_coercions : bool ref
Sourceval print_parentheses : bool ref
Sourceval print_universes : bool ref
Sourceval print_no_symbol : bool ref
Sourceval print_projections : bool ref
Sourceval print_raw_literal : bool ref
Sourceval set_extern_reference : (?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid) -> unit

Customization of the global_reference printer

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

WARNING: The following functions are evil due to side-effects. Think of the following case as used in the printer:

without_specific_symbols SynDefRule kn (pr_glob_constr_env env) c

vs

without_specific_symbols SynDefRule kn pr_glob_constr_env env c

which one is wrong? We should turn this kind of state into an explicit argument.

Sourceval with_universes : ('a -> 'b) -> 'a -> 'b

This forces printing universe names of Type{.}

Sourceval without_symbols : ('a -> 'b) -> 'a -> 'b

This suppresses printing of primitive tokens and notations

Sourceval without_specific_symbols : Notation.interp_rule list -> ('a -> 'b) -> 'a -> 'b

This suppresses printing of specific notations only

Sourceval with_meta_as_hole : ('a -> 'b) -> 'a -> 'b

This prints metas as anonymous holes

Sourceval toggle_scope_printing : scope:Notation_term.scope_name -> activate:bool -> unit

Fine-grained activation and deactivation of notation printing.

Sourceval toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit -> unit
Sourceval empty_extern_env : extern_env

Probably shouldn't be used

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct