]> matita.cs.unibo.it Git - helm.git/commit
cicEnvironment refactoring with sound view of Coq`s univ-less terms
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 18 Apr 2008 15:30:40 +0000 (15:30 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 18 Apr 2008 15:30:40 +0000 (15:30 +0000)
commitafcc11c0cf6751122dc3907f130b819851099a49
tree5e2f6c845949688a5ac1ac2887ca06021280bda5
parentca1359de73c1c9deda30c9aaff2606b8dd5253bc
cicEnvironment refactoring with sound view of Coq`s univ-less terms
helm/software/components/cic_acic/doubleTypeInference.ml
helm/software/components/cic_proof_checking/cicEnvironment.ml
helm/software/components/cic_proof_checking/cicEnvironment.mli
helm/software/components/cic_proof_checking/cicTypeChecker.ml