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/refiner.ml | |
| 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/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 13 |
1 files changed, 0 insertions, 13 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, |