X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=225c1898e022f78fa5758e5d51c83e9b8e2afa31;hb=a806d6607af696065af3c9b0e3373de2846bf174;hp=757fceea2a4a5dd83e728fb88e069a7f28f54957;hpb=25592452b14808ddddcb5bf16b91c8c184be249f;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 757fceea2..225c1898e 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -18,17 +18,27 @@ exception AssertFailure of string Lazy.t;;
 module C = NCic
 module Ref = NReference
 
+let debug = ref false;;
 let indent = ref "";;
-let inside c = indent := !indent ^ String.make 1 c;;
-let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
+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 ^ " ")
+;;
+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 := "??"; ()
+;;
 
-let debug = ref false;;
-let pp s = 
-  if !debug then
-    prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
-  else 
-    ()
-;;  
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
@@ -94,7 +104,7 @@ let check_allowed_sort_elimination rdb localise r orig =
         with exc -> raise (wrap_exc (lazy (localise orig, 
           "Sort elimination not allowed ")) exc))
      | _ -> assert false
-     (*D*)in outside(); rc with exc -> outside (); raise exc
+     (*D*)in outside true; rc with exc -> outside false; raise exc
    in
     aux
 ;;
@@ -119,7 +129,7 @@ let rec typeof rdb
              let metasenv, subst =
     (*D*)inside 'U'; try let rc = 
                NCicUnification.unify rdb metasenv subst context infty expty 
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
              in
              metasenv, subst, t, expty
            with 
@@ -128,7 +138,7 @@ let rec typeof rdb
              try_coercions rdb ~localise 
                metasenv subst context t orig infty expty true exc)
     | None -> metasenv, subst, t, infty
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
   in
   let rec typeof_aux metasenv subst context expty = 
     fun t as orig -> 
@@ -366,7 +376,7 @@ let rec typeof rdb
     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
+    (*D*)in outside true; rc with exc -> outside false; raise exc
   in
     typeof_aux metasenv subst context expty term
 
@@ -579,7 +589,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
     List.partition (fun (i,_) -> i <= highest_meta) metasenv
    in
     (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty
-  (*D*)in outside(); rc with exc -> outside (); raise exc
+  (*D*)in outside true; rc with exc -> outside false; raise exc
 ;;
 
 let rec first f l1 l2 =