package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val __coq_plugin_name : string
val fail_default_value : int Locus.or_var
val genarg_of_unit : unit -> Genarg.rlevel Genarg.generic_argument
val genarg_of_int : int -> Genarg.rlevel Genarg.generic_argument
val reference_to_id : Libnames.qualid -> Names.Id.t CAst.t
val new_entry : string -> 'a Pcoq.Entry.t
val toplevel_selector : Goal_select.t Pcoq.Entry.t
val tacdef_body : Tacexpr.tacdef_body Pcoq.Entry.t
val classic_proof_mode : Pvernac.proof_mode
val test_bracket_ident : unit Pcoq.Entry.t
val print_info_trace : int option ref
val vernac_solve : pstate:Proof_global.t -> Goal_select.t -> int option -> Tacexpr.raw_tactic_expr -> bool -> Proof_global.t
val pr_ltac_selector : Goal_select.t -> Pp.t
val wit_ltac_selector : (Goal_select.t, unit, unit) Genarg.genarg_type
val ltac_selector : Goal_select.t Pcoq.Entry.t
val pr_ltac_info : int -> Pp.t
val wit_ltac_info : (int, unit, unit) Genarg.genarg_type
val ltac_info : int Pcoq.Entry.t
val pr_ltac_use_default : bool -> Pp.t
val wit_ltac_use_default : (bool, unit, unit) Genarg.genarg_type
val ltac_use_default : bool Pcoq.Entry.t
val is_anonymous_abstract : < constant : 'a ; dterm : 'b ; level : 'c ; name : 'd ; pattern : 'e ; reference : 'f ; tacexpr : 'g ; term : 'h > Tacexpr.gen_tactic_expr -> bool
val rm_abstract : < constant : 'a ; dterm : 'b ; level : 'c ; name : 'd ; pattern : 'e ; reference : 'f ; tacexpr : 'g ; term : 'h > Tacexpr.gen_tactic_expr -> 'i Tacexpr.gen_tactic_expr
val is_explicit_terminator : < constant : 'a ; dterm : 'b ; level : 'c ; name : 'd ; pattern : 'e ; reference : 'f ; tacexpr : 'g ; term : 'h > Tacexpr.gen_tactic_expr -> bool
val pr_ltac_tactic_level : int -> Pp.t
val wit_ltac_tactic_level : (int, unit, unit) Genarg.genarg_type
val ltac_tactic_level : int Pcoq.Entry.t
val wit_ltac_production_sep : (string, unit, unit) Genarg.genarg_type
val ltac_production_sep : string Pcoq.Entry.t
val pr_ltac_production_item : (string * string option) Tacentries.grammar_tactic_prod_item_expr -> Pp.t
val wit_ltac_production_item : ((string * string option) Tacentries.grammar_tactic_prod_item_expr, unit, unit) Genarg.genarg_type
val ltac_production_item : (string * string option) Tacentries.grammar_tactic_prod_item_expr Pcoq.Entry.t
val pr_ltac_ref : Libnames.qualid -> Pp.t
val pr_tacdef_body : Environ.env -> Evd.evar_map -> Tacexpr.tacdef_body -> Pp.t
val wit_ltac_tacdef_body : (Tacexpr.tacdef_body, unit, unit) Genarg.genarg_type
val ltac_tacdef_body : Tacexpr.tacdef_body 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