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

(limited to 'engine/eConstr.mli')

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