added some messages

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 72a6409efbbf1b80446df87fce8d649af3a7400a..c8f6bdb59eb763e99cc03d7875804e6c412452f8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -22,12 +22,14 @@ 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 wrap_exc msg = function
@@ -171,7 +173,7 @@ let rec typeof
          force_to_sort ~look_for_coercion
            metasenv subst context1 t orig_t localise s2 in
        let metasenv, subst, s, t, ty = 
-         sort_of_prod ~look_for_coercion localise metasenv subst 
+         sort_of_prod localise metasenv subst 
            context orig_s orig_t (name,s) t (s1,s2)
        in
        metasenv, subst, NCic.Prod(name,s,t), ty
@@ -300,9 +302,23 @@ and try_coercions
         (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
   | (metasenv, newterm, newtype, meta)::tl ->
       try 
+          pp (lazy ( "UNIFICATION in CTX:\n"^ 
+            NCicPp.ppcontext ~metasenv ~subst context
+            ^ "\nMENV: " ^
+            NCicPp.ppmetasenv metasenv ~subst
+            ^ "\nOF: " ^
+            NCicPp.ppterm ~metasenv ~subst ~context meta ^  " === " ^
+            NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
         let metasenv, subst = 
           NCicUnification.unify metasenv subst context meta t
         in
+          pp (lazy ( "UNIFICATION in CTX:\n"^ 
+            NCicPp.ppcontext ~metasenv ~subst context
+            ^ "\nMENV: " ^
+            NCicPp.ppmetasenv metasenv ~subst
+            ^ "\nOF: " ^
+            NCicPp.ppterm ~metasenv ~subst ~context newtype ^  " === " ^
+            NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
         let metasenv, subst = 
           if perform_unification then
             NCicUnification.unify metasenv subst context newtype expty
@@ -340,7 +356,7 @@ and force_to_sort
          "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
          ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
 
-and sort_of_prod ~look_for_coercion
+and sort_of_prod 
   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) 
 =
    (* force to sort is done in the Prod case in typeof *)