diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 | ||||
| -rw-r--r-- | proofs/goal.ml | 2 |
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 |