From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 13 Jun 2008 12:01:37 +0000 (+0000)
Subject: replace assert false with AssertFailure
X-Git-Tag: make_still_working~5029
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbe46eaa76d94ea97c7aa1d60bdcbde9380a2e14;p=helm.git

replace assert false with AssertFailure
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a70fe03ae..87b3f7f42 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1627,7 +1627,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                    | 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)