X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=eb7b136c28f3ba948c9048a5f247241614181499;hb=e1ffde2ba67b8a2f7d4d97898ba28afd65d96ea7;hp=253af6f37cdec2cefea9deed14191e7e166f2346;hpb=1ee5193677b8e2a80d4f068ee79ecac335de1196;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 253af6f37..eb7b136c2 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -22,11 +22,13 @@ 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 = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
+*)
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
@@ -292,6 +294,9 @@ let rec typeof
               let ty_branch = 
                 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 ty_branch ));
               let metasenv, subst, p, _ = 
                 typeof_aux metasenv subst context (Some ty_branch) p in
               j+1, metasenv, subst, p :: branches)
@@ -327,8 +332,8 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
           in
           let flex_prod = C.Prod ("_", ty_arg, meta) in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
-            NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
-            NCicPp.ppmetasenv ~subst metasenv ^ "\nOF: " ^
+            NCicPp.ppcontext ~metasenv ~subst context
+            ^ "\nOF: " ^
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
           let metasenv, subst =