X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fextraction.ma;h=2af7f4a1828a96c4de9058ad6ea8362172560c00;hb=a78228fa1d53da35b589f8b5f29816270f467af8;hp=aa781cfa7469ce8b40226a74e480d01bf8c52b23;hpb=e7fb8e2fdb6fafa0c38bf06146169a0a4efc6b38;p=helm.git

diff --git a/matita/matita/lib/extraction.ma b/matita/matita/lib/extraction.ma
index aa781cfa7..2af7f4a18 100644
--- a/matita/matita/lib/extraction.ma
+++ b/matita/matita/lib/extraction.ma
@@ -186,4 +186,23 @@ axiom lt: nat → nat → Prop.
 (*BUG: elimination principles not extracted *)
 inductive myvect (A: Type[0]) (b:nat) : nat → Type[0] ≝
    myemptyv : myvect A b O
- | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
\ No newline at end of file
+ | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
+ 
+inductive False: Prop ≝ .
+
+inductive Empty: Type[0] ≝ .
+
+inductive bool: Type[0] ≝ true: bool | false:bool.
+
+inductive eq (A:Type[1]) (a:A) : A → Prop ≝ refl: eq A a a.
+
+(* BUG: requires coercion *)
+definition cast_bug1 ≝
+ λH:eq Type[0] bool nat. S (match H return λA:Type[0].λ_.A with [ refl ⇒ true ]).
+
+(* BUG: requires top type *)
+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