package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val tactic_kw : string list
val err : unit -> 'a
val test_lpar_id_coloneq : unit Pcoq.Gram.Entry.e
val test_lpar_id_rpar : unit Pcoq.Gram.Entry.e
val test_lpar_idnum_coloneq : unit Pcoq.Gram.Entry.e
val check_for_coloneq : unit Pcoq.Gram.Entry.e
val lookup_at_as_comma : unit Pcoq.Gram.Entry.e
val mkNumeral : int -> Constrexpr.prim_token
val mkTacCase : Tacexpr.evars_flag -> (Constrexpr.constr_expr_r CAst.t, Constrexpr.constr_expr_r CAst.t, 'a) Tacexpr.induction_clause_list -> < constant : 'b ; dterm : Constrexpr.constr_expr_r CAst.t ; level : 'c ; name : 'a ; pattern : 'd ; reference : 'e ; tacexpr : 'f ; term : Constrexpr.constr_expr_r CAst.t > Tacexpr.gen_atomic_tactic_expr
val loc_of_ne_list : 'a CAst.t list -> Loc.t option
val map_int_or_var : ('a -> 'b) -> 'a Locus.or_var -> 'b Locus.or_var
val all_concl_occs_clause : 'a Locus.clause_expr
val merge_occurrences : Loc.t -> 'a Locus.clause_expr -> (Locus.occurrences_expr * 'b) option -> 'b option * 'a Locus.clause_expr
val warn_deprecated_eqn_syntax : ?loc:Loc.t -> string -> unit
OCaml

Innovation. Community. Security.