diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-02 16:01:06 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-02 16:01:06 +0000 |
| commit | b467ab92ef5bd124ae2bd19deea58765bd034f83 (patch) | |
| tree | 2099a3c260b119f0f9a163fbef7d29691059e94b | |
| parent | 90dc97de5055999d374470ac3a4099057c87091f (diff) | |
Fixing constr_cmp, propagating subtyping only right of a product
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11425 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/termops.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 654cd2b1a..d18ee4fde 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -947,9 +947,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 - | _ -> false) - || compare_constr (constr_cmp cv_pb) t1 t2 + 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 let eq_constr = constr_cmp Reduction.CONV |