package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val register_ltac : Vernacexpr.locality_flag -> ?deprecation:Deprecation.t -> Tacexpr.tacdef_body list -> unit
type !'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
  1. | TacTerm of string
  2. | TacNonTerm of ('a * Names.Id.t option) Loc.located
type raw_argument = string * string option
val add_tactic_notation : Vernacexpr.locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument grammar_tactic_prod_item_expr list -> Tacexpr.raw_tactic_expr -> unit
val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -> unit
val add_ml_tactic_notation : Tacexpr.ml_tactic_name -> level:int -> ?deprecation:Deprecation.t -> argument grammar_tactic_prod_item_expr list list -> unit
val create_ltac_quotation : string -> ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit
val print_ltacs : unit -> unit
val print_located_tactic : Libnames.qualid -> unit
type (!_, !'a1) ml_ty_sig =
  1. | MLTyNil : ('a, 'a) ml_ty_sig
  2. | MLTyArg : ('r, 'a0) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a0) ml_ty_sig
val ml_tactic_extend : plugin:string -> name:string -> local:Vernacexpr.locality_flag -> ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit
val ml_val_tactic_extend : plugin:string -> name:string -> local:Vernacexpr.locality_flag -> ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit
type !_ ty_sig =
  1. | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
  2. | TyIdent : string * 'r ty_sig -> 'r ty_sig
  3. | TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r0 ty_sig -> ('c -> 'r0) ty_sig
type ty_ml =
  1. | TyML : 'r ty_sig * 'r -> ty_ml
val tactic_extend : string -> string -> level:Int.t -> ?deprecation:Deprecation.t -> ty_ml list -> unit
type (!'a1, !'b1) argument_intern =
  1. | ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern
  2. | ArgInternWit : ('a0, 'b0, 'c) Genarg.genarg_type -> ('a0, 'b0) argument_intern
type !'b1 argument_subst =
  1. | ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
  2. | ArgSubstWit : ('a, 'b0, 'c) Genarg.genarg_type -> 'b0 argument_subst
type (!'b2, !'c3) argument_interp =
  1. | ArgInterpRet : ('c, 'c) argument_interp
  2. | ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c0) argument_interp
  3. | ArgInterpWit : ('a, 'b0, 'r) Genarg.genarg_type -> ('b0, 'c1) argument_interp
  4. | ArgInterpLegacy : (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b1 -> Evd.evar_map * 'c2) -> ('b1, 'c2) argument_interp
type (!'a, !'b, !'c) tactic_argument = {
  1. arg_parsing : 'a Vernacextend.argument_rule;
  2. arg_tag : 'c Geninterp.Val.tag option;
  3. arg_intern : ('a, 'b) argument_intern;
  4. arg_subst : 'b argument_subst;
  5. arg_interp : ('b, 'c) argument_interp;
  6. arg_printer : ('a, 'b, 'c) argument_printer;
}
val argument_extend : name:string -> ('a, 'b, 'c) tactic_argument -> ('a, 'b, 'c) Genarg.genarg_type * 'a Pcoq.Entry.t
OCaml

Innovation. Community. Security.