3 files changed, 19 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ae7446c82..e68be91e9b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -97,9 +97,6 @@ let _ =
 
 (* Rewriting tactics *)
 
-let tclNOTSAMEGOAL tac =
-  Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac))
-
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
 type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 
@@ -268,6 +265,25 @@ let rewrite_elim with_evars frzevars cls c e =
   general_elim_clause with_evars flags cls c e
   end }
 
+let tclNOTSAMEGOAL tac =
+  let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = project gl in
+    let ev = goal gl in
+    tac >>= fun () ->
+    Proofview.Goal.goals >>= fun gls ->
+    let check accu gl' =
+      gl' >>= fun gl' ->
+      let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in
+      Proofview.tclUNIT accu
+    in
+    Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
+    if has_same then
+      tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
+    else
+      Proofview.tclUNIT ()
+  end }
+
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars frzevars cls rew elim =
   let open Pretype_errors in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 90b7d6581a..97922a4fa5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -54,7 +54,6 @@ let tclDO            = Refiner.tclDO
 let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
-let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
 let tclTHENTRY       = Refiner.tclTHENTRY
 let tclIFTHENELSE    = Refiner.tclIFTHENELSE
 let tclIFTHENSELSE   = Refiner.tclIFTHENSELSE
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3b90ec514a..33933924ab 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -47,7 +47,6 @@ val tclDO            : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic