From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 May 2008 16:47:54 +0000 (+0000)
Subject: wrong test equality only fixed
X-Git-Tag: make_still_working~5226
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0ac9442fc6cc033a3a5bb9d7288b9ce5da99767;p=helm.git

wrong test equality only fixed
---

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index bd2498c04..32c553367 100644
--- 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 &&