aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-17 20:51:40 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-17 20:51:40 +0200
commitf96dc97f48df5d0fdf252be5f28478a58be77961 (patch)
tree5d741e02de71083b5e279121721dff7cb4b56516 /proofs
parent17f68d403d248e899efbb76afeed169232946ecf (diff)
Fix bug #3593, making constr_eq and progress work up to
equality of universes, along with a few other functions in evd.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/goal.ml2
2 files changed, 3 insertions, 3 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 612ef8d7d..5a7572eb2 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -167,7 +167,7 @@ let clenv_assign mv rhs clenv =
error "clenv_assign: circularity in unification";
try
if meta_defined clenv.evd mv then
- if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+ if not (eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
error_incompatible_inst clenv mv
else
clenv
@@ -480,7 +480,7 @@ let clenv_match_args bl clenv =
(fun clenv (loc,b,c) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
- if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+ if eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
else error_already_defined b
else
clenv_assign_binding clenv k c)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 55de87261..dea704a68 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -94,7 +94,7 @@ let solution sigma g =
let equal evars1 gl1 evars2 gl2 =
let evi1 = content evars1 gl1 in
let evi2 = content evars2 gl2 in
- Evd.eq_evar_info evi1 evi2
+ Evd.eq_evar_info evars2 evi1 evi2
(* [contained_in_info e evi] checks whether the evar [e] appears in
the hypotheses, the conclusion or the body of the evar_info