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

val deprecated_clear_modifier : ?loc:Loc.t -> unit -> unit