From 38a2e8c383228e9cb3a3437d981d30a488f5a084 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 28 Oct 2018 15:01:04 +0100
Subject: [error printing] Fix improper grounding of open terms in printing.

Fixes #8224, fixes #8427 .
---
 vernac/himsg.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ca77e03707..45eaa4ba1e 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 *)
-- 
cgit v1.2.3