From: Claudio Sacerdoti Coen Date: Mon, 27 Aug 2012 16:26:23 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~1537 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68419a627d2c76d09e022f4489bffb28b877f0ef;p=helm.git ... --- diff --git a/matita/matita/lib/extraction.ma b/matita/matita/lib/extraction.ma index 2af7f4a18..08a76e0ec 100644 --- a/matita/matita/lib/extraction.ma +++ b/matita/matita/lib/extraction.ma @@ -205,4 +205,7 @@ definition cast_bug2 ≝ λb. match true return λb.match b with [ true ⇒ nat → nat | false ⇒ bool ] with [ true ⇒ S | false ⇒ false ] - O. \ No newline at end of file + O. + +(*BUG: try singleton elimination with constructor arguments to show bug in + DeBrujin indexes *) \ No newline at end of file