From 552544a3d385a3a59def038bdb0a22a69fe4b0a9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 16:42:24 +0100
Subject: Removing the tclNOTSAMEGOAL primitive from the API.

The only use in Equality is reimplemented in the new engine.
---
 proofs/refiner.ml  | 13 -------------
 proofs/refiner.mli |  1 -
 2 files changed, 14 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5c7659ac0e..d086f0bbca 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 56f5facf89..de6502dc36 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,
-- 
cgit v1.2.3