diff options
| author | Gaëtan Gilbert | 2019-02-26 23:41:38 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-25 10:53:19 +0100 |
| commit | bf840bafc19deba67e5270dfd31b8b6662b73132 (patch) | |
| tree | 0b35aa63d6faa37356b4b87d763e47577809f6d2 /proofs/goal.ml | |
| parent | e8fd832d9e487fa57e2efe627223d04ff2977fa9 (diff) | |
Fix #9652: rewrite fails to detect lack of progress
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 11 |
1 files changed, 1 insertions, 10 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 = |