From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Aug 2012 14:35:46 +0000 (+0000)
Subject: Basics/logic.ma no longer raises exception.
X-Git-Tag: make_still_working~1529
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=631c6fe57fd0b63deb9592fd8f59c1821e7536db;p=helm.git

Basics/logic.ma no longer raises exception.
Many workaround introduced to feed arguments to polymorphically kinded functions.
---

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index 7f76392ca..53498362e 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -157,7 +157,8 @@ let rec classify_not_term status context t =
   | NCic.LetIn _
   | NCic.Lambda _
   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
-  | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
+  | NCic.Appl [] ->
+     assert false (* NOT POSSIBLE *)
   | NCic.Match _
   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
      (* be aware: we can be the head of an application *)
@@ -538,8 +539,19 @@ and eat_args status metasenv acc context tyhe =
            | _ -> term_of status ~metasenv context arg in
          eat_args status metasenv (mk_appl acc arg) context t tl
       | Forall (_,_,t) ->
-         eat_args status metasenv (Inst acc)
-          context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
+         (match classify status ~metasenv context arg with
+           | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
+           | `Proposition
+           | `Term `TypeFormer
+           | `Kind ->
+               eat_args status metasenv (UnsafeCoerce (Inst acc))
+                context (fomega_subst 1 Unit t) tl
+           | `Term _ -> assert false (*TODO: ????*)
+           | `KindOrType
+           | `Type ->
+               eat_args status metasenv (Inst acc)
+                context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
+                 tl)
       | TSkip t ->
          eat_args status metasenv acc context t tl
       | Top -> assert false (*TODO: HOW??*)