]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a405885) | patch
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
tree40ddd250c088473491b21a924ce24a71b381643btree | snapshot
parenta4058857e32cec5492821cf11696cdb25df28f4ccommit | diff
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 diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.