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 18e9f92cbc1ffbb229d89823b52f5b5351b80647..9e43d0e24e6ef4a596d0f127007b1980924e642a 100644 (file)
--- 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