]> matita.cs.unibo.it Git - helm.git/commitdiff
Meta case not handled, the iterator was complaining.
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Aug 2009 10:50:03 +0000 (10:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Aug 2009 10:50:03 +0000 (10:50 +0000)
helm/software/components/ng_kernel/nCicTypeChecker.ml

index 695b2e5319f61df33cdd05115c4058c2cf94adbd..6dbaf3e5d05a702c45ac967d581e60a578955466 100644 (file)
@@ -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 ->