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 c2c3902e47df7432a4c224f48dcc0af2d2eff64a..3d58e9acf8522950a911499122c1abb464ed5cd6 100644 (file)
--- 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