Thu, 09 Jun 2011 00:16:28 +0200 removed more dead code
blanchet [Thu, 09 Jun 2011 00:16:28 +0200] rev 43300
removed more dead code
Thu, 09 Jun 2011 00:16:28 +0200 be a bit more liberal with respect to the universal sort -- it sometimes help
blanchet [Thu, 09 Jun 2011 00:16:28 +0200] rev 43299
be a bit more liberal with respect to the universal sort -- it sometimes help
Thu, 09 Jun 2011 00:16:28 +0200 renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
blanchet [Thu, 09 Jun 2011 00:16:28 +0200] rev 43298
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
Wed, 08 Jun 2011 22:13:49 +0200 merged
wenzelm [Wed, 08 Jun 2011 22:13:49 +0200] rev 43297
merged
Wed, 08 Jun 2011 17:01:07 +0200 avoid duplicate facts, which confuse the minimizer output
blanchet [Wed, 08 Jun 2011 17:01:07 +0200] rev 43296
avoid duplicate facts, which confuse the minimizer output
Wed, 08 Jun 2011 16:20:19 +0200 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet [Wed, 08 Jun 2011 16:20:19 +0200] rev 43295
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
Wed, 08 Jun 2011 16:20:18 +0200 restore comment about subtle issue
blanchet [Wed, 08 Jun 2011 16:20:18 +0200] rev 43294
restore comment about subtle issue
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip