G_tactic (coq-core.Ltac_plugin.G

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) -> '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 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