summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4198.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/4198.v')
-rw-r--r--test-suite/bugs/closed/4198.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index f85a6026..eb37141b 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -11,7 +11,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
simpl.
intros.
match goal with
- | [ |- appcontext G[@hd] ] => idtac
+ | [ |- context G[@hd] ] => idtac
end.
(* This second example comes from CFGV where inspecting subterms of a