]> matita.cs.unibo.it Git - helm.git/commit
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
tree6aef323af8f797b0a454d486f0042d50ba06dc65
parent50ed5ab75a38693c7b7558ca9487998e81bb7f89
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
helm/software/components/ng_kernel/nCicEnvironment.mli
helm/software/components/ng_kernel/nCicTypeChecker.ml
helm/software/components/ng_tactics/nCicElim.ml