Removing the tclNOTSAMEGOAL primitive from the API.

The only use in Equality is reimplemented in the new engine.

5 files changed, 19 insertions, 19 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5c7659ac0..d086f0bbc 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -174,19 +174,6 @@ let tclPROGRESS tac ptree =
   if Goal.V82.progress rslt ptree then rslt
   else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
 
-(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
-   one of them being identical to the original goal *)
-let tclNOTSAMEGOAL (tac : tactic) goal =
-  let same_goal gls1 evd2 gl2 =
-    Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2
-  in
-  let rslt = tac goal in
-  let {it=gls;sigma=sigma} = rslt in
-  if List.exists (same_goal goal sigma) gls
-  then user_err ~hdr:"Refiner.tclNOTSAMEGOAL"
-      (str"Tactic generated a subgoal identical to the original goal.")
-  else rslt
-
 (* Execute tac, show the names of new hypothesis names created by tac
    in the "as" format and then forget everything. From the logical
    point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 56f5facf8..de6502dc3 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -122,7 +122,6 @@ val tclDO            : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ae7446c8..e68be91e9 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 90b7d6581..97922a4fa 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 3b90ec514..33933924a 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