From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 24 Nov 2004 13:18:03 +0000 (+0000)
Subject: guard get_cooked_obj calls with assert false in case of Not_found
X-Git-Tag: PRE_UNIVERSES~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c0ca8e4ddc55168bc3e5eb32c435b5befee1d01;p=helm.git

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 5d3d40a10..e4dbee6ef 100644
--- 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)