X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=7c199f8c07bf0c64ec295392f99083ad81b20db8;hb=f3cddcf163b36101158ea33b3fad368ac8c62d75;hp=5a6f1028fdf9a4ad177a2483961a090096f8a697;hpb=aff007d80f87128884c96a664bc88aec69107d85;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 5a6f1028f..7c199f8c0 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -109,7 +109,7 @@ let rec typeof rdb
        | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
        | C.Appl _ when skip_appl -> metasenv, subst, t, expty
        | _ ->
-          pp (lazy (
+          pp (lazy ("forcing infty=expty: "^
           (NCicPp.ppterm ~metasenv ~subst ~context infty) ^  " === " ^
           (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
            try 
@@ -126,7 +126,7 @@ let rec typeof rdb
   let rec typeof_aux metasenv subst context expty = 
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
-    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " expty= " ^
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
        match expty with None -> "None" | Some e -> 
        NCicPp.ppterm ~metasenv ~subst ~context e));
     let metasenv, subst, t, infty = 
@@ -332,7 +332,7 @@ let rec typeof rdb
                 NCicTypeChecker.type_of_branch 
                   ~subst context leftno outtype cons ty_cons in
               pp (lazy ("TYPEOFBRANCH: " ^
-               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^
+               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^
                NCicPp.ppterm ~metasenv ~subst ~context ty_branch ));
               let metasenv, subst, p, _ = 
                 typeof_aux metasenv subst context (Some ty_branch) p in
@@ -344,7 +344,7 @@ let rec typeof rdb
       metasenv, subst, C.Match (r, outtype, term, pl),resty
     | C.Match _ -> assert false
     in
-    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty true true metasenv subst context orig t infty expty
     (*D*)in outside(); rc with exc -> outside (); raise exc
@@ -467,7 +467,9 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
        " of type " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_he
        ^ " to type " ^ match expty with None -> "None" | Some x -> 
        NCicPp.ppterm ~metasenv ~subst ~context x));
-      force_ty true false metasenv subst context orig_t res ty_he expty
+     (* whatever the term is, we force the type. in case of ((Lambda..) ?...)
+      * the application may also be a lambda! *)
+     force_ty false false metasenv subst context orig_t res ty_he expty
   | NCic.Implicit `Vector::tl ->
       let has_some_more_pis x =
         match NCicReduction.whd ~subst context x with
@@ -520,7 +522,11 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
               (NCicPp.ppterm ~metasenv ~subst ~context he)
               (NCicPp.ppterm ~metasenv ~subst ~context t)
               (NCicPp.ppterm ~metasenv ~subst ~context arg)
-              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
+              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) 
+                 (match exc with
+                 | NCicUnification.UnificationFailure m -> 
+                     NCicUnification.Uncertain m
+                 | x -> x))
               (* XXX coerce to funclass *)
           in
           let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in