From 55c3395a0151d9943702ed87342471f1b15f3802 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 May 2008 11:34:37 +0000 Subject: [PATCH] types where compared without lookig at test_eq_only --- helm/software/components/ng_kernel/nCicReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2