]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 407e4f0) | 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)
commitdd1c4eeef3d38eb9e01d50d06de6892a048c05a5
tree3e10505d75d130649fac55f330f21e67a96c9dcatree | snapshot
parent407e4f0b8f189b38fcffd6438afce4bc4aa83f01commit | 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.
components/cic_proof_checking/cicPp.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.