]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8230675) | patch
1. Some warnings about unused warning fixed (hopefully well)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 13 Sep 2006 14:08:57 +0000 (14:08 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 13 Sep 2006 14:08:57 +0000 (14:08 +0000)
commit8b9d2632ab7edc7102d16f3857fde02139cef5c2
tree16370d8a2d76f8b00bdce15e77f3e1ee92dd2611tree | snapshot
parent82306753608353e9aed7e1b9c03b96787f1ec5ebcommit | diff
1. Some warnings about unused warning fixed (hopefully well)
2. We now try to print the MutCase in the new syntax.
   This fails silently when the type of the constructor is not a spine of Prods
   ended by something not convertible to another Prod. It also fails providing
   reasonable information when one pattern has not enough Lambdas.
helm/software/components/cic_proof_checking/cicPp.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.