diff options
| author | Matthieu Sozeau | 2014-09-17 22:26:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-17 22:26:18 +0200 |
| commit | d9736dae4168927f735ca4f60b61a83929ae4435 (patch) | |
| tree | 4afd85aee98945c458f210261ccc4265298e4475 /proofs | |
| parent | f96dc97f48df5d0fdf252be5f28478a58be77961 (diff) | |
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 5a7572eb23..3ef3466340 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 clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then + if not (Term.eq_constr (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 clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv + if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv else error_already_defined b else clenv_assign_binding clenv k c) |