From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Aug 2012 14:25:45 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~1540
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a78228fa1d53da35b589f8b5f29816270f467af8

...
---

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
diff --git a/matita/matita/lib/preamble.hs b/matita/matita/lib/preamble.hs
index 2aea1bb44..abc288aa4 100644
--- a/matita/matita/lib/preamble.hs
+++ b/matita/matita/lib/preamble.hs
@@ -1,5 +1,7 @@
-{-# LANGUAGE RankNTypes, KindSignatures #-}
+{-# LANGUAGE RankNTypes, KindSignatures, GADTs, ScopedTypeVariables #-}
 
 module Main where
 
-
+import Unsafe.Coerce
+import Prelude (error)
+import qualified Prelude