diff options
-rw-r--r-- | plugins/micromega/Env.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/closed/2839.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/3563.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/closed/4198.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_020.v | 4 | ||||
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_058.v | 10 | ||||
-rw-r--r-- | test-suite/bugs/opened/3383.v | 2 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 2 | ||||
-rw-r--r-- | theories/Program/Wf.v | 2 |
9 files changed, 18 insertions, 18 deletions
diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v index a19e9df90..7e3ef8929 100644 --- a/plugins/micromega/Env.v +++ b/plugins/micromega/Env.v @@ -93,7 +93,7 @@ End S. Ltac jump_simpl := repeat match goal with - | |- appcontext [jump xH] => rewrite (jump_simpl xH) - | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p)) - | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p)) + | |- context [jump xH] => rewrite (jump_simpl xH) + | |- context [jump (xO ?p)] => rewrite (jump_simpl (xO p)) + | |- context [jump (xI ?p)] => rewrite (jump_simpl (xI p)) end. diff --git a/test-suite/bugs/closed/2839.v b/test-suite/bugs/closed/2839.v index e396fe06e..e727e2606 100644 --- a/test-suite/bugs/closed/2839.v +++ b/test-suite/bugs/closed/2839.v @@ -5,6 +5,6 @@ intro. Fail let H := match goal with - | [ H : appcontext G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' + | [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H' end in pose H. diff --git a/test-suite/bugs/closed/3563.v b/test-suite/bugs/closed/3563.v index 679721667..961563ed4 100644 --- a/test-suite/bugs/closed/3563.v +++ b/test-suite/bugs/closed/3563.v @@ -16,11 +16,11 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0) transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ] => set(foo:=h); idtac end. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ] + | [ |- context ctx [transport (fun y => (?g (fst (y H2))))] ] => idtac end. Abort. @@ -30,7 +30,7 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0) transport (fun y : H1 -> (H1 -> H) * H0 => H5 (fst (y H2) H2)) H4 H6 = H7. intros. match goal with - | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] + | [ |- context ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ] => set(foo:=X) end. (* Anomaly: Uncaught exception Not_found(_). Please report. *) 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 diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 008fb72c4..73da464bb 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -22,8 +22,8 @@ Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := o Ltac present_obj from to := match goal with - | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * - | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * + | [ _ : context[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in * + | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * end. Section NaturalTransformationComposition. diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v index 5e5d5ab3e..3d16e7ac0 100644 --- a/test-suite/bugs/closed/HoTT_coq_058.v +++ b/test-suite/bugs/closed/HoTT_coq_058.v @@ -95,10 +95,10 @@ Goal forall (T : Type) (T0 : T -> T -> Type) | tt => idpath end)) (x1; p) = (x1; p). intros. -let F := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in -let H := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in -let X := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in -let T := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in +let F := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in +let H := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in +let X := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in +let T := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in let t0 := fresh "t0" in let t1 := fresh "t1" in let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in @@ -116,7 +116,7 @@ let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in let GL1' := fresh in set (GL0' := GL0); - let arg := match GL0 with appcontext[x0 ?arg] => constr:(arg) end in + let arg := match GL0 with context[x0 ?arg] => constr:(arg) end in assert (t1 = arg) by (subst t1; reflexivity); subst t1; pattern (x0 arg) in GL0'; match goal with diff --git a/test-suite/bugs/opened/3383.v b/test-suite/bugs/opened/3383.v index 9a14641a5..c04b6b7b4 100644 --- a/test-suite/bugs/opened/3383.v +++ b/test-suite/bugs/opened/3383.v @@ -1,7 +1,7 @@ Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end. intro. Fail lazymatch goal with -| [ |- appcontext[match ?b as b' return @?P b' with true => ?t | false => ?f end] ] +| [ |- context[match ?b as b' return @?P b' with true => ?t | false => ?f end] ] => change (match b as b' return P b with true => t | false => f end) with (@bool_rect P t f) end. (* Toplevel input, characters 153-154: Error: The reference P was not found in the current environment. *) diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 7384790da..dfd6b0eae 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -264,7 +264,7 @@ Ltac bang := match goal with | |- ?x => match x with - | appcontext [False_rect _ ?p] => elim p + | context [False_rect _ ?p] => elim p end end. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index a2fd05cd9..c490ea516 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -211,7 +211,7 @@ Ltac fold_sub f := match goal with | [ |- ?T ] => match T with - appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] => + context C [ @Fix_sub _ _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end |