fixed Ref generation

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 58036784f634e8e8427f3c86d4987ac0fce35d0b..757fceea2a4a5dd83e728fb88e069a7f28f54957 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -22,13 +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 debug = ref false;;
 let pp s = 
-  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+  if !debug then
+    prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+  else 
+    ()
 ;;  
 
-let pp _ = ();;
-
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
   | NCicUnification.UnificationFailure _ -> RefineFailure msg
@@ -242,7 +243,8 @@ let rec typeof rdb
          | Some x -> 
              let m, s, x = 
                NCicUnification.delift_type_wrt_terms 
-                 rdb metasenv subst context x [t]
+                rdb metasenv subst context1 (NCicSubstitution.lift 1 x)
+                [NCicSubstitution.lift 1 t]
              in
                m, s, Some x
        in
@@ -376,7 +378,7 @@ and try_coercions rdb
   let rec first exc = function
   | [] ->         
       raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
-        "The term %s has type %s but is here used with type %s"
+        "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
         (NCicPp.ppterm ~metasenv ~subst ~context t)
         (NCicPp.ppterm ~metasenv ~subst ~context infty)
         (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)