Merge PR #8834: [error printing] Fix improper grounding of open terms in printing.

1 files changed, 2 insertions, 3 deletions

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 844caf5a3e..ad6ca3a84e 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -391,11 +391,10 @@ let explain_unexpected_type env sigma actual_type expected_type =
   str "where" ++ spc () ++ prexp ++ str " was expected."
 
 let explain_not_product env sigma c =
-  let c = EConstr.to_constr sigma c in
-  let pr = pr_lconstr_env env sigma c in
+  let pr = pr_econstr_env env sigma c in
   str "The type of this term is a product" ++ spc () ++
   str "while it is expected to be" ++
-  (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
+  (if EConstr.isType sigma c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
 
 (* TODO: use the names *)
 (* (co)fixpoints *)