From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 11 Jun 2008 09:24:08 +0000 (+0000)
Subject: meta not considered before in outtype
X-Git-Tag: make_still_working~5040
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=102a4101f6b4b7da9861de73054188df470c4462;p=helm.git

meta not considered before in outtype
---

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