From f535df7a8249f365bf63c9d6bb2a0f080364594d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Aug 2009 10:50:03 +0000 Subject: [PATCH] Meta case not handled, the iterator was complaining. --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 ++++ 1 file changed, 4 insertions(+) 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 -> -- 2.39.2