From e8680015a9f4da6e50d9e1baa5affb9075445894 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 25 Nov 2004 09:00:35 +0000
Subject: [PATCH] protected invocations of get_cooked_obj with assertion
 failures

---
 helm/ocaml/cic_unification/cicRefine.ml | 35 +++++++++++++++++++++----
 1 file changed, 30 insertions(+), 5 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index dd510797a..0f751b996 100644
--- 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
           | _ ->
-- 
2.39.2