]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 50ed5ab) | patch
1) The NG kernel now accepts only usage of declared universes
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 Jul 2009 16:25:26 +0000 (16:25 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 Jul 2009 16:25:26 +0000 (16:25 +0000)
commit2ee517d852ad53540881221ecb01b9ec1881cc6a
tree6aef323af8f797b0a454d486f0042d50ba06dc65tree | snapshot
parent50ed5ab75a38693c7b7558ca9487998e81bb7f89commit | diff
1) The NG kernel now accepts only usage of declared universes
2) Bug (badly) fixed in NCicElim: it used to generate undeclared universe
   names.
helm/software/components/ng_kernel/nCicEnvironment.ml diff | blob | history
helm/software/components/ng_kernel/nCicEnvironment.mli diff | blob | history
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
helm/software/components/ng_tactics/nCicElim.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.