diff options
| author | Pierre-Marie Pédrot | 2014-09-04 15:22:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 15:22:07 +0200 |
| commit | f3b714f5a8e516ee9731d705808a4084caae5a1e (patch) | |
| tree | 5811499a4d0d97f4b6b5de73beab3b32a6ce456e | |
| parent | c9d9e0ffa4bd3efb9366726f3c78374d71f87b8b (diff) | |
More explicit printing in Himsg.
| -rw-r--r-- | toplevel/himsg.ml | 4 |
1 files 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 () ++ |