[error printing] Fix improper grounding of open terms in printing.

Fixes #8224, fixes #8427 .

2 files changed, 10 insertions, 0 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 3385b78958..cfc4bea85f 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -99,6 +99,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false
 let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false
 let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
 let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
+
+let rec isType sigma c = match kind sigma c with
+  | Sort s -> (match ESorts.kind sigma s with
+      | Sorts.Type _ -> true
+      | _ -> false )
+  | Cast (c,_,_) -> isType sigma c
+  | _ -> false
+
 let isVarId sigma id c =
   match kind sigma c with Var id' -> Id.equal id id' | _ -> false
 let isRelN sigma n c =
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 1edc0ee12b..6532e08e9d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -157,6 +157,8 @@ val isCoFix : Evd.evar_map -> t -> bool
 val isCase : Evd.evar_map -> t -> bool
 val isProj : Evd.evar_map -> t -> bool
 
+val isType : Evd.evar_map -> constr -> bool
+
 type arity = rel_context * ESorts.t
 val destArity : Evd.evar_map -> types -> arity
 val isArity : Evd.evar_map -> t -> bool