From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Oct 2006 07:20:13 +0000 (+0000)
Subject: 1. some "try ... with _ " removed
X-Git-Tag: 0.4.95@7852~930
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00d48171bacce45b5e7fcc17d841694aee4dba70;p=helm.git

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
---

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index c2c3902e4..3d58e9acf 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/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