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
| 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
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)