package coq

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

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

val extern_env : Environ.env -> Evd.evar_map -> extern_env
val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a Glob_term.glob_constr_g -> Constrexpr.constr_expr
val 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

val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_expr
val extern_constr_in_scope : ?lax:bool -> ?inctx: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 : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Constrexpr.constr_expr
val extern_sort : Evd.evar_map -> Sorts.t -> Constrexpr.sort_expr
val print_implicits : bool ref

Printing options

val print_implicits_defensive : bool ref
val print_arguments : bool ref
val print_evar_arguments : bool ref
val print_coercions : bool ref
val print_parentheses : bool ref
val print_universes : bool ref
val print_no_symbol : bool ref
val print_projections : bool ref
val print_raw_literal : bool 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

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.

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