]> matita.cs.unibo.it Git - helm.git/commit
Types for LetIns computed during parsing for Coq objects may contain universes
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Apr 2008 09:41:34 +0000 (09:41 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Apr 2008 09:41:34 +0000 (09:41 +0000)
commit3c31a89866838b8f2d190cad359836d898eb1b93
tree6ec6119c8b068631327235f5128e277fc477d6a0
parent86e962200667fbd6d77f9680d08f6d5efc59959c
Types for LetIns computed during parsing for Coq objects may contain universes
that must be made fresh.
helm/software/components/cic/deannotate.ml