From d67b1c5ba2ac0886389ae24274cd869ce819b6af Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 28 Nov 2007 21:08:18 +0000 Subject: [PATCH] Bug fixed: an unification exception used to escape during eat_prods. --- .../components/cic_unification/cicRefine.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index d52b8aa7c..4569601cd 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1204,14 +1204,16 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (fun (metasenv,last,coerc) -> let pp t = CicMetaSubst.ppterm_in_context ~metasenv subst t context in - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last he ugraph in - debug_print (lazy ("New head: "^ pp coerc)); try + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last he ugraph in + debug_print (lazy ("New head: "^ pp coerc)); let tty,ugraph = - CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in - debug_print (lazy (" has type: "^ pp tty)); - Some (coerc,tty,subst,metasenv,ugraph) + CicTypeChecker.type_of_aux' ~subst metasenv context coerc + ugraph + in + debug_print (lazy (" has type: "^ pp tty)); + Some (coerc,tty,subst,metasenv,ugraph) with | Uncertain _ | RefineFailure _ | HExtlib.Localized (_,Uncertain _) -- 2.39.2