guard get_cooked_obj calls with assert false in case of Not_found

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5d3d40a106f3c7af6db019e2021cafc54014ad44..e4dbee6ef96e8ed1870a37010bd2ca74f08d345d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1005,7 +1005,12 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
       let consty =
-       match CicEnvironment.get_cooked_obj ~trust:false uri with
+       let obj =
+         try
+           CicEnvironment.get_cooked_obj ~trust:false uri
+         with Not_found -> assert false
+       in
+       match obj with
           C.InductiveDefinition (itl,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
             let (_,cons) = List.nth cl (j - 1) in
@@ -1537,7 +1542,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t =
           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
         (* let's check if the type of branches are right *)
       let parsno =
-        match CicEnvironment.get_cooked_obj ~trust:false uri with
+        let obj =
+          try
+            CicEnvironment.get_cooked_obj ~trust:false uri
+          with Not_found -> assert false
+        in
+        match obj with
             C.InductiveDefinition (_,_,parsno) -> parsno
           | _ ->
               raise (TypeCheckerFailure
@@ -1727,7 +1737,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t =
    match CicReduction.whd context ty with
       C.MutInd (uri,i,_) ->
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
-       (match CicEnvironment.get_cooked_obj ~trust:false uri with
+        let obj =
+          try
+            CicEnvironment.get_cooked_obj ~trust:false uri
+          with Not_found -> assert false
+        in
+        (match obj with
            C.InductiveDefinition (itl,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)