From 8dbc4dcef7328f3ac84f847255e9be8d47c1de6d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 6 May 2010 15:45:35 +0000
Subject: [PATCH] assert false could happen

---
 helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index cd49f2cea..02eec0576 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1304,7 +1304,9 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
             | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as ref) :: _) ->
                 let _,_,itl,_,_ = E.get_checked_indtys ref in
                   uri, List.length itl
-            | _ -> assert false
+            | _ ->
+              raise (TypeCheckerFailure
+               (lazy "Fix: the recursive argument is not inductive"))
           in
           (* guarded by destructors conditions D{f,k,x,M} *)
           let rec enum_from k = 
-- 
2.39.2