From b467ab92ef5bd124ae2bd19deea58765bd034f83 Mon Sep 17 00:00:00 2001 From: puech Date: Thu, 2 Oct 2008 16:01:06 +0000 Subject: 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 --- pretyping/termops.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3