From 102a4101f6b4b7da9861de73054188df470c4462 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 11 Jun 2008 09:24:08 +0000 Subject: [PATCH] meta not considered before in outtype --- helm/software/components/cic_unification/cicRefine.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index b5204de02..a70fe03ae 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1623,8 +1623,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci CicTypeChecker.type_of_aux' ~subst metasenv context m CicUniv.oblivion_ugraph with - | Cic.MutInd _ as mty,_ -> [], mty - | Cic.Appl (Cic.MutInd _::args) as mty,_ -> + | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty + | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ -> snd (HExtlib.split_nth leftno args), mty | _ -> assert false with CicTypeChecker.TypeCheckerFailure _ -> assert false -- 2.39.2