wrong test equality only fixed

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index bd2498c04e5b73d244e9e0ccc8ff45d294a9376d..32c553367234305bfa19cf846041ea68056f44df 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -504,7 +504,7 @@ let are_convertible whd ?(subst=[])  =
            aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
           aux true context s1 s2 && 
-          aux true ((name1, C.Decl s1)::context) t1 t2
+          aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
           aux test_equality_only context ty1 ty2 &&
           aux test_equality_only context s1 s2 &&