removed unused variable

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index b5204de02f78baa2a6731d25c5e61bfe7aa11cef..87b3f7f42a319f227f06ce9d9c7b3db5bfc85e53 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1623,11 +1623,12 @@ 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
+                 with CicTypeChecker.TypeCheckerFailure _ -> 
+                    raise (AssertFailure(lazy "already ill-typed matched term"))
                in
                let new_outty =
                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)