diff options
| author | Emilio Jesus Gallego Arias | 2019-04-02 12:15:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-02 12:15:58 +0200 |
| commit | 32dbd76a5df76491e029583abf247524f8d26c44 (patch) | |
| tree | 25185fd3ad82c6c5e2e39ed35c0c2eccf5064ea1 /proofs | |
| parent | 424c1973e96dfbf3b2e3245d735853ffa9600373 (diff) | |
| parent | bf840bafc19deba67e5270dfd31b8b6662b73132 (diff) | |
Merge PR #9659: Fix #9652: rewrite fails to detect lack of progress
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 11 | ||||
| -rw-r--r-- | proofs/goal.mli | 3 |
2 files changed, 1 insertions, 13 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index e5688fe730..94707accab 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -89,18 +89,9 @@ module V82 = struct | None -> sigma | Some id -> Evd.rename evk' id sigma - (* Parts of the progress tactical *) - let same_goal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in - let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in - Constr.equal c1 c2 && - Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps - let weak_progress glss gls = match glss.Evd.it with - | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it) + | [ g ] -> not (Proofview.Progress.goal_equal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it) | _ -> true let progress glss gls = diff --git a/proofs/goal.mli b/proofs/goal.mli index af9fb662bf..665b0c9e59 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -57,9 +57,6 @@ module V82 : sig (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool - (* Principal part of tclNOTSAMEGOAL *) - val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool - (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map |