]> matita.cs.unibo.it Git - helm.git/commit
CicUniv.UniverseInconsistency is no handled correcly.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Oct 2006 20:23:24 +0000 (20:23 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Oct 2006 20:23:24 +0000 (20:23 +0000)
commit37018b8195f0f376d9eb04a98cbda5550f7ac8ef
tree5b78916d79c17eb48a9ec37085dde8848eead8ab
parentf030d33d2c43fbfe8daa2891f036529b733c5852
CicUniv.UniverseInconsistency is no handled correcly.
helm/software/components/cic/cicUniv.ml
helm/software/components/cic/cicUniv.mli
helm/software/components/cic_proof_checking/cicReduction.ml
helm/software/components/cic_proof_checking/cicTypeChecker.ml
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/cic_unification/cicUnification.ml
helm/software/components/tactics/primitiveTactics.ml