X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=3d58e9acf8522950a911499122c1abb464ed5cd6;hb=2bd3b029f7f67d9c616b7756278573cc9e96510c;hp=bd8e992d0bfdef7d8b3eddc39a0a4b4c1a25ed90;hpb=456f7d82d3cf6732daa36bb07d06c23c4a60beda;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index bd8e992d0..3d58e9acf 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -34,8 +34,8 @@ exception AssertFailure of string Lazy.t;;
 let insert_coercions = ref true
 let pack_coercions = ref true
 
-(* let debug_print = fun _ -> () *)
- let debug_print x = prerr_endline (Lazy.force x);; 
+let debug_print = fun _ -> ();;
+(*let debug_print x = prerr_endline (Lazy.force x);;*)
 
 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
 
@@ -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 
@@ -1492,7 +1494,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
      else
        (* this (says CSC) is also useful to infer dependent types *)
-       fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+       try
+        fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+       with RefineFailure _ | Uncertain _ as exn ->
+         (* unable to fix arity *)
+          more_args_than_expected localization_tbl 
+            subst he context hetype args_bo_and_ty exn
     in
     let coerced_args,subst,metasenv,he,t,ugraph =
       eat_prods_and_args 
@@ -1724,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