X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=c3765f3f0261eb092bbb93e87c8e12df6d0a9bc7;hb=d00e19c7000a00659ffd609ef79675eb0f010659;hp=b88e261f102d2d39b58e24b081f90e750e273ef5;hpb=818403f4064a0aecbd316f239127a67b8cbfe34c;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index b88e261f1..c3765f3f0 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -20,23 +20,33 @@ module Ref = NReference
 
 let debug = ref false;;
 let indent = ref "";;
+let times = ref [];;
 let pp s =
  if !debug then
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
- else 
-  ()
 ;;
 let inside c =
- indent := !indent ^ String.make 1 c;
- if !debug then prerr_endline ("{{{" ^ !indent ^ " ")
+ if !debug then
+  begin
+   let time1 = Unix.gettimeofday () in
+   indent := !indent ^ String.make 1 c;
+   times := time1 :: !times;
+   prerr_endline ("{{{" ^ !indent ^ " ")
+  end
 ;;
 let outside ok =
- if !debug then prerr_endline "}}}";
- if not ok then pp (lazy "exception raised!");
- try
-  indent := String.sub !indent 0 (String.length !indent -1)
- with
-  Invalid_argument _ -> indent := "??"; ()
+ if !debug then
+  begin
+   let time2 = Unix.gettimeofday () in
+   let time1 =
+    match !times with time1::tl -> times := tl; time1 | [] -> assert false in
+   prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+   if not ok then prerr_endline "exception raised!";
+   try
+    indent := String.sub !indent 0 (String.length !indent -1)
+   with
+    Invalid_argument _ -> indent := "??"; ()
+ end
 ;;
 
 
@@ -537,7 +547,10 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
            aux metasenv subst args_so_far he ty_he
             (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl)
           with
-           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc)))
+           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
+     | RefineFailure msg when not (has_some_more_pis ty_he) ->
+        (* instantiating the head could change the has_some_more_pis flag *)
+        raise (Uncertain msg))
   | arg::tl ->
       match NCicReduction.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->