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 .
---
 engine/eConstr.ml  | 8 ++++++++
 engine/eConstr.mli | 2 ++
 2 files changed, 10 insertions(+)

(limited to 'engine')

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
-- 
cgit v1.2.3