From 2a12ea82de3c63b05b06e3a21e434dd56b427568 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 6 Oct 2006 07:20:13 +0000 Subject: [PATCH] 1. some "try ... with _ " removed 2. type inference of LetIn terms is now closer than the kernel 3. LetIn code fixed to add the type to the Defs in the environment 4. some typos fixed --- .../components/cic_unification/cicRefine.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index c2c3902e4..3d58e9acf 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -78,6 +78,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = match exn with RefineFailure msg -> RefineFailure (f msg) | Uncertain msg -> Uncertain (f msg) + | Sys.Break -> raise exn | _ -> assert false in let loc = try @@ -357,9 +358,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy "Rel to hidden hypothesis")) with - _ -> + Failure _ -> enrich localization_tbl t - (RefineFailure (lazy "Not a close term"))) + (RefineFailure (lazy "Not a closed term"))) | C.Var (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst @@ -578,8 +579,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t * Even faster than the previous solution. * Moreover the inferred type is closer to the expected one. *) - C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, - subst'',metasenv'',ugraph2 + C.LetIn (n,s',t'), + CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty, + subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> let he',hetype,subst',metasenv',ugraph1 = type_of_aux subst metasenv context he ugraph @@ -1729,7 +1731,9 @@ let pack_coercion metasenv ctx t = let ctx' = (Some (name,C.Decl so))::ctx in C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) | C.LetIn (name,so,dest) -> - let ctx' = Some (name,(C.Def (so,None)))::ctx in + let _,ty,metasenv,ugraph = + type_of_aux' metasenv ctx so CicUniv.empty_ugraph in + let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest) | C.Appl l -> let l = List.map (merge_coercions ctx) l in -- 2.39.2