From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Aug 2009 10:50:03 +0000 (+0000)
Subject: Meta case not handled, the iterator was complaining.
X-Git-Tag: make_still_working~3522
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f535df7a8249f365bf63c9d6bb2a0f080364594d;p=helm.git

Meta case not handled, the iterator was complaining.
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 695b2e531..6dbaf3e5d 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -256,6 +256,10 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
   let dummy = C.Sort C.Prop in
   (*CSC: to be moved in cicSubstitution? *)
   let rec subst_inductive_type_with_dummy _ = function
+    | C.Meta (_,(_,C.Irl _)) as x -> x
+    | C.Meta (i,(lift,C.Ctx ls)) -> 
+        C.Meta (i,(lift,C.Ctx 
+          (List.map (subst_inductive_type_with_dummy ()) ls)))
     | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
     | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl) 
         when NUri.eq uri' uri ->