diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-07 16:42:24 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-24 17:55:38 +0200 |
commit | 552544a3d385a3a59def038bdb0a22a69fe4b0a9 (patch) | |
tree | 6098a4029f9dc05f320b992b969900d0ec37e250 /proofs | |
parent | e57074289193b0f0184f3c7143d8ab7e0edd5112 (diff) |
Removing the tclNOTSAMEGOAL primitive from the API.
The only use in Equality is reimplemented in the new engine.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/refiner.ml | 13 | ||||
-rw-r--r-- | proofs/refiner.mli | 1 |
2 files changed, 0 insertions, 14 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, |