From e0ac9442fc6cc033a3a5bb9d7288b9ce5da99767 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2008 16:47:54 +0000 Subject: [PATCH] wrong test equality only fixed --- 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 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 && -- 2.39.2