From 0703cd1bbe5aab7e584d2293fe76c5f6ac4fe08c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Aug 2018 18:51:04 +0200
Subject: Reworking error message for unresolved evar subterm of another evar.

This is a reworking of 7fd28dc9: instead of using words such as
"domain of", "codomain of" to refer to a position in the instance of
the original evar, we simply display the instance and the name of the
unresolved evar in this instance. This is both simpler and more
informative. (The positional words remain useful for printing the
evar_map in debugging though.)

In passing, this fixes #8369 (Not_found in printing message about an
unresolved subevar).

Incidentally add possible breaking while printing "in environment".
---
 test-suite/bugs/closed/bug_8369.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_8369.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v
new file mode 100644
index 0000000000..9816954d0c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8369.v
@@ -0,0 +1,3 @@
+(* Was failing in master with a not_found generated by the printer *)
+
+Fail Definition foo := fun '(u, v) p2 => (u, v).
-- 
cgit v1.2.3