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 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'engine/eConstr.ml')

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