Merge PR #13379: Add a new evar source to refer to evars which are types of evars

Reviewed-by: SkySkimmer

1 files changed, 9 insertions, 0 deletions

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).