diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 22:44:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:10:43 +0100 |
| commit | aa99912e9adc566a179b4972ff85a92b967fb134 (patch) | |
| tree | 96a0f2264ce398bd8d6f1a86c5be1fa5aff7391f /tactics/tactics.mli | |
| parent | e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 (diff) | |
Removing redundant versions of generalize.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 129837d08..f06a50f79 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -385,7 +385,8 @@ val letin_pat_tac : (bool * intro_pattern_naming) option -> (** {6 Generalize tactics. } *) val generalize : constr list -> tactic -val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic +val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic + val new_generalize : constr list -> unit Proofview.tactic val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic @@ -417,9 +418,6 @@ module Simple : sig (** Simplified version of some of the above tactics *) val intro : Id.t -> unit Proofview.tactic - val generalize : constr list -> tactic - val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic - val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic val elim : constr -> unit Proofview.tactic |