package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val extern_closed_glob : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Constrexpr.constr_expr
val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constrexpr.constr_expr
val print_implicits : bool ref
val print_implicits_defensive : bool ref
val print_arguments : bool ref
val print_evar_arguments : bool ref
val print_coercions : bool ref
val print_universes : bool ref
val print_no_symbol : bool ref
val print_projections : bool ref
val set_extern_reference : (?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference) -> unit
val get_extern_reference : unit -> ?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference
val with_universes : ('a -> 'b) -> 'a -> 'b
val without_symbols : ('a -> 'b) -> 'a -> 'b
val without_specific_symbols : Notation.interp_rule list -> ('a -> 'b) -> 'a -> 'b
val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
val toggle_scope_printing : scope:Notation_term.scope_name -> activate:bool -> unit
val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
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