Module Ltac_plugin.G_tactic

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.tConstrexpr.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