diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 61f3e4a02..19f816a01 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -99,7 +99,7 @@ module V82 = struct let same_goal evars1 gl1 evars2 gl2 = let evi1 = Evd.find evars1 gl1 in let evi2 = Evd.find evars2 gl2 in - Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl && + Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl && Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps let weak_progress glss gls = |