From 47910007a9eff37c9f364a269b46874165711abf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Nov 2020 16:14:48 +0100
Subject: Add a new evar source to refer to evars which are types of evars.

To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.

An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
---
 test-suite/success/evars.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 253b48e4d9..2308656f7c 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -426,3 +426,12 @@ Abort.
 (* (reported as bug #7356) *)
 
 Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z).
+
+(* A printing check in passing *)
+
+Axiom abs : forall T, T.
+Fail Type let x := _ in
+     ltac:(
+       let t := type of x in
+       unify x (abs t);
+     exact 0).
-- 
cgit v1.2.3