Thu, 07 Nov 2013 01:01:04 +0100 blanchet more docs
Thu, 07 Nov 2013 00:37:18 +0100 blanchet properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
Wed, 06 Nov 2013 23:05:44 +0100 blanchet reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip