package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac_plugin.G_ltacSource

Sourceval fail_default_value : int Locus.or_var
Sourceval genarg_of_unit : unit -> Genarg.rlevel Genarg.generic_argument
Sourceval genarg_of_int : int -> Genarg.rlevel Genarg.generic_argument
Sourceval reference_to_id : Libnames.qualid -> Names.Id.t CAst.t
Sourceval new_entry : string -> 'a Pcoq.Entry.t
Sourceval toplevel_selector : Goal_select.t Pcoq.Entry.t
Sourceval tacdef_body : Tacexpr.tacdef_body Pcoq.Entry.t
Sourceval classic_proof_mode : Pvernac.proof_mode
Sourceval test_bracket_ident : unit Pcoq.Entry.t
Sourceval for_extraargs : unit
Sourceval pr_ltac_selector : Goal_select.t -> Pp.t
Sourceval wit_ltac_selector : (Goal_select.t, unit, unit) Genarg.genarg_type
Sourceval ltac_selector : Goal_select.t Pcoq.Entry.t
Sourceval pr_ltac_info : int -> Pp.t
Sourceval wit_ltac_info : (int, unit, unit) Genarg.genarg_type
Sourceval ltac_info : int Pcoq.Entry.t
Sourceval pr_ltac_use_default : bool -> Pp.t
Sourceval wit_ltac_use_default : (bool, unit, unit) Genarg.genarg_type
Sourceval ltac_use_default : bool Pcoq.Entry.t
Sourceval 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 * bool
Sourceval is_explicit_terminator : < constant : 'a ; dterm : 'b ; level : 'c ; name : 'd ; pattern : 'e ; reference : 'f ; tacexpr : 'g ; term : 'h > Tacexpr.gen_tactic_expr_r CAst.t -> bool
Sourceval pr_ltac_tactic_level : int -> Pp.t
Sourceval wit_ltac_tactic_level : (int, unit, unit) Genarg.genarg_type
Sourceval ltac_tactic_level : int Pcoq.Entry.t
Sourceval wit_ltac_production_sep : (string, unit, unit) Genarg.genarg_type
Sourceval ltac_production_sep : string Pcoq.Entry.t
Sourceval pr_ltac_production_item : (string * string option) Tacentries.grammar_tactic_prod_item_expr -> Pp.t
Sourceval check_non_empty_string : ?loc:Loc.t -> string -> unit
Sourceval wit_ltac_production_item : ((string * string option) Tacentries.grammar_tactic_prod_item_expr, unit, unit) Genarg.genarg_type
Sourceval ltac_production_item : (string * string option) Tacentries.grammar_tactic_prod_item_expr Pcoq.Entry.t
Sourceval pr_ltac_ref : Libnames.qualid -> Pp.t
Sourceval pr_tacdef_body : Environ.env -> Evd.evar_map -> Tacexpr.tacdef_body -> Pp.t
Sourceval wit_ltac_tacdef_body : (Tacexpr.tacdef_body, unit, unit) Genarg.genarg_type
Sourceval 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