Wed, 05 Sep 2012 11:37:22 +0200 | blanchet | made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation) | changeset | files |
Wed, 05 Sep 2012 11:18:48 +0200 | blanchet | tuning (systematic 1-based indices) | changeset | files |