From f3b714f5a8e516ee9731d705808a4084caae5a1e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Sep 2014 15:22:07 +0200
Subject: More explicit printing in Himsg.

---
 toplevel/himsg.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f50423b3d4..11abe09503 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -472,8 +472,8 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   let vdefj = Evarutil.jv_nf_evar sigma vdefj in
   let vargs = Array.map (Evarutil.nf_evar sigma) vargs in
   let env = make_all_name_different env in
-  let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in
-  let pv = pr_lconstr_env env vargs.(i) in
+  let pvd = pr_lconstr_env env vdefj.(i).uj_val in
+  let pvdt, pv = pr_explicit env vdefj.(i).uj_type vargs.(i) in
   str "The " ++
   (match vdefj with [|_|] -> mt () | _ -> pr_nth (i+1) ++ spc ()) ++
   str "recursive definition" ++ spc () ++ pvd ++ spc () ++
-- 
cgit v1.2.3