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