diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-18 00:53:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-18 00:57:24 +0200 |
| commit | a07af57f3140a2481e1e2f45a930a17d80a33645 (patch) | |
| tree | 5ea91c9bede1cbf1aa1991b7c3875fb20bedf8e5 /test-suite/bugs/closed/4198.v | |
| parent | ddf50c8bb15ce86fc3e3fbedf9f86fd278f01776 (diff) | |
Fix bug #4923: Warning: appcontext is deprecated.
Diffstat (limited to 'test-suite/bugs/closed/4198.v')
| -rw-r--r-- | test-suite/bugs/closed/4198.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index f85a60264..eb37141bc 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 |