From f46a5686853353f8de733ae7fbd21a3a61977bc7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 15:32:58 +0100 Subject: Do not give a name to anonymous evars anymore. See bug #4547. The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced. --- test-suite/success/destruct.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'test-suite/success/destruct.v') diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 9f091e399..90a60daa6 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -96,21 +96,21 @@ Abort. (* Check that subterm selection does not solve existing evars *) Goal exists x, S x = S 0. -eexists. +eexists ?[x]. Show x. (* Incidentally test Show on a named goal *) destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S 0). Abort. Goal exists x, S 0 = S x. -eexists. +eexists ?[x]. destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S ?x). [x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. -do 2 eexists. +eexists ?[n]; eexists ?[p]. destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *) change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n). Abort. @@ -426,7 +426,7 @@ destruct b eqn:H. (* Check natural instantiation behavior when the goal has already an evar *) Goal exists x, S x = x. -eexists. +eexists ?[x]. destruct (S _). change (0 = ?x). Abort. -- cgit v1.2.3