...

[helm.git] / matita / matita / lib / extraction.ma

diff --git a/matita/matita/lib/extraction.ma b/matita/matita/lib/extraction.ma
index 2af7f4a1828a96c4de9058ad6ea8362172560c00..08a76e0ecb1721d4bc0686c3149b7863c2052a55 100644 (file)
--- 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