package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
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 Stdlib.ref
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_parentheses : 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
val get_extern_reference : unit -> ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
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
val empty_extern_env : extern_env
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