]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a23d480) | patch
impredicative Set is considered as Prop in the new check implemented by CSC
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 May 2008 18:50:09 +0000 (18:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 May 2008 18:50:09 +0000 (18:50 +0000)
commit23fa8cfe44a11df5a93d349e2520011e6722e096
tree23a3e37ad83d2bd41b773c885da6520641e60497tree | snapshot
parenta23d480c6fb31b878ff4e72c796dfb8f83034238commit | diff
impredicative Set is considered as Prop in the new check implemented by CSC
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.