From c1e3eafa4990b4e1e41d589c0e1a20b641ea1493 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 17 Sep 2010 18:03:40 +0000 Subject: Fixed a problem introduced in r12607 after pattern_of_constr served both for interpreting ltac patterns and patterns of "change pat with term". In particular, in the current status, Goal evars needs mandatorily to have the hole_kind GoalEvar. If this is too complicated to enforce, we might eventually consider another approach to the question of interpreting patterns in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13428 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/ltac.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 32c6d1431..a8d1ba7f5 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -281,3 +281,20 @@ Goal forall x:nat, True. intro x. Fail clear x; f x. Abort. + +(* Do not consider evars as unification holes in Ltac matching (and at + least not as holes unrelated to the original evars) + [Example adapted from Ynot code] + *) + +Ltac not_eq e1 e2 := + match e1 with + | e2 => fail 1 + | _ => idtac + end. + +Goal True. +evar(foo:nat). +let evval := eval compute in foo in not_eq evval 1. +let evval := eval compute in foo in not_eq 1 evval. +Abort. -- cgit v1.2.3