Module `Ltac_plugin.G_tactic`

val all_with : 'a Genredexpr.red_atom -> 'a Genredexpr.glob_red_flag
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 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) -> 'a * 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) -> 'a * 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 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 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 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 -> 'b option * 'a Locus.clause_expr