diff options
| author | herbelin | 2011-10-25 13:50:38 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-25 13:50:38 +0000 |
| commit | 801cee9983f6b99101d783c12bc5e094cebe59e7 (patch) | |
| tree | 623d3f47cbb434acdf77460bb434f3422796c70d | |
| parent | 1ae71d6b88f79ceedad611bbf1a9128800a275b0 (diff) | |
Fixing "destruct" test.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14594 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/destruct.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index b4217e6df5..fc40ea964f 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -89,7 +89,7 @@ Goal (exists x, x=0 /\ True) -> True. destruct 1 as (_,(_,x)); exact x. Abort. -Goal let T:=nat in forall (x:nat) (f:T -> nat), f x = 0. +Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0. intros. -destruct (f _). (* This was failing in at least r14571 *) +destruct (g _). (* This was failing in at least r14571 *) Abort. |