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