From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 May 2008 11:34:37 +0000 (+0000)
Subject: types where compared without lookig at test_eq_only
X-Git-Tag: make_still_working~5192
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55c3395a0151d9943702ed87342471f1b15f3802;p=helm.git

types where compared without lookig at test_eq_only
---

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 18e9f92cb..9e43d0e24 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -495,7 +495,7 @@ let are_convertible whd ?(subst=[])  =
        true
      else
        match (t1,t2) with
-       | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
+       | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> a <= b
        | (C.Sort s1,C.Sort (C.Type _)) -> (not test_eq_only)
        | (C.Sort s1, C.Sort s2) -> s1 = s2