X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fextraction.ma;h=08a76e0ecb1721d4bc0686c3149b7863c2052a55;hb=68419a627d2c76d09e022f4489bffb28b877f0ef;hp=2af7f4a1828a96c4de9058ad6ea8362172560c00;hpb=efdc4b8deed29fbcd4b2673e1f174696cd4c67d6;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