From b0c458c8ba160bfac2ba3ab3d20af6224e9b4ac4 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 25 Nov 2004 09:05:18 +0000 Subject: [PATCH] protected invocations to get_cooked_obj with assertion failures --- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index ea29f46fa..5b0cc01fc 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -541,7 +541,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Checks suppressed *) (* Let's visit all the subterms that will not be visited later *) let (cl,parsno) = - 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 (tl,_,parsno) -> let (_,_,_,cl) = List.nth tl i in (cl,parsno) | _ -> @@ -639,14 +644,24 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = and visit_exp_named_subst context uri exp_named_subst = let uris_and_types = - match CicEnvironment.get_cooked_obj uri with + let obj = + try + CicEnvironment.get_cooked_obj uri + with Not_found -> assert false + in + match obj with Cic.Constant (_,_,_,params) | Cic.CurrentProof (_,_,_,_,params) | Cic.Variable (_,_,_,params) | Cic.InductiveDefinition (_,params,_) -> List.map (function uri -> - match CicEnvironment.get_cooked_obj uri with + let obj = + try + CicEnvironment.get_cooked_obj uri + with Not_found -> assert false + in + match obj with Cic.Variable (_,None,ty,_) -> uri,ty | _ -> assert false (* the theorem is well-typed *) ) params -- 2.39.2