Module `Ltac_plugin.G_tactic`Source

Sourceval all_with : 'a Genredexpr.red_atom -> 'a Genredexpr.glob_red_flag

Sourceval err : unit -> 'a

Sourceval test_lpar_id_coloneq : unit Pcoq.Entry.t

Sourceval test_lpar_id_rpar : unit Pcoq.Entry.t

Sourceval test_lpar_idnum_coloneq : unit Pcoq.Entry.t

Sourceval check_for_coloneq : unit Pcoq.Entry.t

Sourceval 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

Source

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

Source

val destruction_arg_of_constr : 
  (Constrexpr.constr_expr * 'a Tactypes.bindings) ->
  (Constrexpr.constr_expr * 'a Tactypes.bindings) Tactics.core_destruction_arg

Sourceval mkNumber : int -> Constrexpr.prim_token

Source

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

Source

val mkCLambdaN_simple_loc : 
  ?loc:Loc.t ->
  (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr) list ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Source

val mkCLambdaN_simple : 
  (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr) list ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Sourceval loc_of_ne_list : 'a CAst.t list -> Loc.t option

Sourceval all_concl_occs_clause : 'a Locus.clause_expr

Source

val merge_occurrences : 
  Loc.t ->
  'a Locus.clause_expr ->
  (Locus.occurrences_expr * 'b) option ->
  'b option * 'a Locus.clause_expr

Sourceval deprecated_conversion_at_with : ?loc:Loc.t -> unit -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/G_tactic/index.html

Module `Ltac_plugin.G_tactic`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/G_tactic/index.html

Module Ltac_plugin.G_tacticSource

Module `Ltac_plugin.G_tactic`Source