diff options
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 |