diff options
| author | puech | 2011-07-29 14:24:10 +0000 |
|---|---|---|
| committer | puech | 2011-07-29 14:24:10 +0000 |
| commit | e471d37d1c93966d85b7005b796921ead6c18cfd (patch) | |
| tree | 42c484ed2e0ce7e0824ae9832aa176767091b52e /kernel/typeops.ml | |
| parent | d43147c7fd9b88af4ba42e5bf39e9c83f2c5beb2 (diff) | |
Term_typing, Typeops: replace some generic '=' on constr by eq_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14313 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 85e8e6c885..c9112e86dd 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -475,7 +475,7 @@ and execute_array env = array_fold_map' (execute env) let infer env constr = let (j,(cst,_)) = execute env constr (empty_constraint, universes env) in - assert (j.uj_val = constr); + assert (eq_constr j.uj_val constr); ({ j with uj_val = constr }, cst) let infer_type env constr = |