From bbe46eaa76d94ea97c7aa1d60bdcbde9380a2e14 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Jun 2008 12:01:37 +0000 Subject: [PATCH] replace assert false with AssertFailure --- helm/software/components/cic_unification/cicRefine.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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) -- 2.39.2