]> matita.cs.unibo.it Git - helm.git/commit
Incredible bug fixed in Fix and CoFix. The types of the mutual inductive
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Feb 2007 18:46:35 +0000 (18:46 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Feb 2007 18:46:35 +0000 (18:46 +0000)
commita2079b129bcb754d55a5ed5290d8b9aaa525ac3e
tree40ddd250c088473491b21a924ce24a71b381643b
parenta4058857e32cec5492821cf11696cdb25df28f4c
Incredible bug fixed in Fix and CoFix. The types of the mutual inductive
functions were not lifted when added to the context.
helm/software/components/cic_proof_checking/cicTypeChecker.ml