]> 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)
commitb7387d913f7dddf52d1e73173bca3fc8729723ba
treef4e6c1cba984b907861af278361a1895ea91dd84
parent1631e7f0f5f841bd0096651429b83b0c166658f7
CicUniv.UniverseInconsistency is no handled correcly.
components/cic/cicUniv.ml
components/cic/cicUniv.mli
components/cic_proof_checking/cicReduction.ml
components/cic_proof_checking/cicTypeChecker.ml
components/cic_unification/cicRefine.ml
components/cic_unification/cicUnification.ml
components/tactics/primitiveTactics.ml