diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-09 16:05:34 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-09 16:05:34 +0000 |
| commit | 2e6c3a7b0b12cfd3b560de60f4918063f149fd01 (patch) | |
| tree | c7dc3dfce59e43a01835278fd59c303373b3dd50 /pretyping/termops.ml | |
| parent | 7f8fb01ffcaa6aeafef0cea9d7169d70ce841537 (diff) | |
* Fixed constr_cmp again to handle universes subtyping correctly
* Fixed typo in unify_0 regarding conv_pb
* First attempt to fix a problem related to rels in w_merge. Seems to
be unsuccessful at this point
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11443 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d18ee4fde..7cbde2d07 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -946,13 +946,12 @@ let base_sort_cmp pb s0 s1 = (* eq_constr extended with universe erasure *) let rec constr_cmp cv_pb t1 t2 = - (match kind_of_term t1, kind_of_term t2 with - Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> - constr_cmp Reduction.CONV t1 t2 & - constr_cmp cv_pb c1 c2 - | _ -> false) - || compare_constr (constr_cmp Reduction.CONV) t1 t2 + match kind_of_term t1, kind_of_term t2 with + Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> + constr_cmp Reduction.CONV t1 t2 & + constr_cmp cv_pb c1 c2 + | _ -> compare_constr (constr_cmp Reduction.CONV) t1 t2 let eq_constr = constr_cmp Reduction.CONV |