]> matita.cs.unibo.it Git - helm.git/commitdiff
Conversion of 2 lambdas was not requiring equality on universes of the source type...
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 11 Apr 2008 10:20:34 +0000 (10:20 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 11 Apr 2008 10:20:34 +0000 (10:20 +0000)
Moreover Coq seems to force that constraint too.

helm/software/components/cic_proof_checking/cicReduction.ml

index 32ae57a4709a18ebd35690fbed84564238468ac2..11fd5123560b1f411bd8a77832c30a6db7150f01 100644 (file)
@@ -909,7 +909,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+           let b',ugraph' = aux true context s1 s2 ugraph in
            if b' then
              aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
                t1 t2 ugraph'