]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ccb0974) | patch
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)
commitff2f125b1c37e7c1406ebca16de7b651802ebc91
tree0469f4ca88cbe256170df50dbda0e4e5ce0b5030tree | snapshot
parentccb09743430d585f773eb83ad9a18d1dbdda07edcommit | diff
Conversion of 2 lambdas was not requiring equality on universes of the source type, while the conversion of products was requiring so.
Moreover Coq seems to force that constraint too.
helm/software/components/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.