Removing redundant versions of generalize.

4 files changed, 6 insertions, 13 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0f907b0ef7..8a4b206010 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -716,7 +716,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
        Tacticals.New.tclTHENLIST
-         [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+         [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
           Proofview.Goal.nf_enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 850580f75d..bfe3097e2e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1932,7 +1932,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Tacticals.New.tclWITHHOLES false
         (name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma
+          (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
       end }
   | TacGeneralizeDep c ->
       (new_interp_constr ist c) (fun c ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c76aeb4a88..539c2ab713 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2647,7 +2647,8 @@ let new_generalize_gen_let lconstr =
   end }
 
 let generalize_gen lconstr =
-  generalize_gen_let (List.map (fun ((occs,c),na) ->
+  generalize_gen_let (List.map (fun (occs_c,na) ->
+    let (occs,c) = Redexpr.out_with_occurrences occs_c in
     (occs,c,None),na) lconstr)
 
 let new_generalize_gen lconstr =
@@ -4652,12 +4653,6 @@ module Simple = struct
 
   let intro x = intro_move (Some x) MoveLast
 
-  let generalize_gen cl =
-    generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)
-  let generalize cl =
-    generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
-                        cl)
-
   let apply c =
     apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))]
   let eapply c =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 129837d082..f06a50f79c 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