package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val __coq_plugin_name : string
val pr_hintbases : 'a -> 'b -> 'c -> string list option -> Pp.t
val wit_hintbases : (string list option, string list option, string list option) Genarg.genarg_type
val hintbases : string list option Pcoq.Entry.t
val pr_auto_using_raw : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> Constrexpr.constr_expr list -> Pp.t
val pr_auto_using_glob : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> ('d Glob_term.glob_constr_g * 'e) list -> Pp.t
val pr_auto_using : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> Ltac_pretype.closed_glob_constr list -> Pp.t
val auto_using : Constrexpr.constr_expr list Pcoq.Entry.t
val make_depth : int option -> int
val deprecated_eauto_bfs : ?loc:Loc.t -> unit -> unit
val deprecated_bfs : string -> ?loc:Loc.t -> unit -> unit
val deprecated_convert_concl_no_check : ?loc:Loc.t -> unit -> unit
val pr_pre_hints_path_atom : 'a -> 'b -> 'c -> Libnames.qualid Hints.hints_path_atom_gen -> Pp.t
val pr_hints_path_atom : 'a -> 'b -> 'c -> Names.GlobRef.t Hints.hints_path_atom_gen -> Pp.t
val pr_hints_path : 'a -> 'b -> 'c -> Hints.hints_path -> Pp.t
val pr_pre_hints_path : 'a -> 'b -> 'c -> Libnames.qualid Hints.hints_path_gen -> Pp.t
val wit_opthints : (string list option, string list option, string list option) Genarg.genarg_type
val opthints : string list option Pcoq.Entry.t
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