package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val err : unit -> 'a
val test_lpar_id_coloneq : unit Pcoq.Entry.t
val test_lpar_id_rpar : unit Pcoq.Entry.t
val test_lpar_idnum_coloneq : unit Pcoq.Entry.t
val check_for_coloneq : unit Pcoq.Entry.t
val lookup_at_as_comma : unit Pcoq.Entry.t
val mkNumber : 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 : 'd ; pattern : 'e ; reference : 'f ; tacexpr : 'g ; 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 all_concl_occs_clause : 'a Locus.clause_expr
val merge_occurrences : Loc.t -> 'a Locus.clause_expr -> (Locus.occurrences_expr * 'b) option -> 'c option * 'a Locus.clause_expr
val deprecated_conversion_at_with : ?loc:Loc.t -> unit -> unit