Ltac_plugin.G_tactic
val all_with : 'a Genredexpr.red_atom -> 'a Genredexpr.glob_red_flag
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 mk_fix_tac :
(Loc.t
* 'a
* (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr) list
* Names.Name.t CAst.t option
* Constrexpr.constr_expr) ->
'b * int * Constrexpr.constr_expr_r CAst.t
val mk_cofix_tac :
(Loc.t
* 'a
* (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr) list
* 'b CAst.t option
* Constrexpr.constr_expr) ->
'c * Constrexpr.constr_expr
val destruction_arg_of_constr :
(Constrexpr.constr_expr * 'a Tactypes.bindings) ->
(Constrexpr.constr_expr * 'a Tactypes.bindings) Tactics.core_destruction_arg
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 mkCLambdaN_simple_loc :
?loc:Loc.t ->
(Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr) list ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr
val mkCLambdaN_simple :
(Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr) list ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr
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
val deprecated_clear_modifier : ?loc:Loc.t -> unit -> unit