diff options
| -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. |