From 5780336e3be522f76906b719c3d3694f243a5bdb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 4 Aug 2018 11:55:46 +0200
Subject: Fixes #8215 ("critical" bug of type inference in interpreting evars
 by names).

When interpreting an existential variable "?n@{inst}" in the current
context, check that variables bound to local definitions are replaced
by variables with convertible body.

Also give a message explaining the type error or non-convertibility
error rather than wrongly saying that there is no binding for the
variable.
---
 test-suite/bugs/closed/8215.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/bugs/closed/8215.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/8215.v b/test-suite/bugs/closed/8215.v
new file mode 100644
index 0000000000..c4b29a6354
--- /dev/null
+++ b/test-suite/bugs/closed/8215.v
@@ -0,0 +1,14 @@
+(* Check that instances for local definitions in evars have compatible body *)
+Goal False.
+Proof.
+  pose (n := 1).
+  evar (m:nat).
+  subst n.
+  pose (n := 0).
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clearbody n.
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clear n.
+  pose (n := 0+1).
+  Check ?m. (* Should be ok *)
+Abort.
-- 
cgit v1.2.3