protected invocations of get_cooked_obj with assertion failures

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index dd510797ab3081370ad3e7efb60e3802e9381099..0f751b9960e8be57dbf54cdb412897ab5d054d88 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -50,7 +50,12 @@ let rec type_of_constant uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
+ let obj =
+   try
+     CicEnvironment.get_cooked_obj uri
+   with Not_found -> assert false
+ in
+  match obj with
      C.Constant (_,_,ty,_) -> ty
    | C.CurrentProof (_,_,_,ty,_) -> ty
    | _ ->
@@ -61,7 +66,12 @@ and type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
+ let obj =
+   try
+     CicEnvironment.get_cooked_obj uri
+   with Not_found -> assert false
+ in
+  match obj with
      C.Variable (_,_,ty,_) -> ty
    |  _ ->
       raise
@@ -72,7 +82,12 @@ and type_of_mutual_inductive_defs uri i =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
+ let obj =
+   try
+     CicEnvironment.get_cooked_obj uri
+   with Not_found -> assert false
+ in
+  match obj with
      C.InductiveDefinition (dl,_,_) ->
       let (_,_,arity,_) = List.nth dl i in
        arity
@@ -85,7 +100,12 @@ and type_of_mutual_inductive_constr uri i j =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
+ let obj =
+   try
+     CicEnvironment.get_cooked_obj uri
+   with Not_found -> assert false
+ in
+  match obj with
       C.InductiveDefinition (dl,_,_) ->
        let (_,_,_,cl) = List.nth dl i in
         let (_,ty) = List.nth cl (j-1) in
@@ -267,7 +287,12 @@ and type_of_aux' metasenv context t =
    | C.MutCase (uri, i, outtype, term, pl) ->
        (* first, get the inductive type (and noparams) in the environment  *)
        let (_,b,arity,constructors), expl_params, no_left_params =
-         match CicEnvironment.get_cooked_obj ~trust:true uri with
+       let obj =
+         try
+           CicEnvironment.get_cooked_obj ~trust:true uri
+         with Not_found -> assert false
+       in
+         match obj with
             C.InductiveDefinition (l,expl_params,parsno) -> 
               List.nth l i , expl_params, parsno
           | _ ->