diff options
| author | Maxime Dénès | 2017-10-30 14:16:48 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-30 14:16:48 +0100 |
| commit | e1b1743fb6aaed042d5e6762ea76c3242593ab1d (patch) | |
| tree | f2c7a9504fe1a1a39a9015a771bf07eba1696ca8 /mathcomp/ssreflect/plugin | |
| parent | d5437703555329168288467dc1a94b1176e1776e (diff) | |
Fix obsolete vernacular syntax for locality.
It was emitting a deprecation warning and will soon be removed from Coq.
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrbool.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.6/ssrbool.v | 10 |
2 files changed, 10 insertions, 10 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrbool.v b/mathcomp/ssreflect/plugin/v8.5/ssrbool.v index c5a881f..f81e16e 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrbool.v +++ b/mathcomp/ssreflect/plugin/v8.5/ssrbool.v @@ -1506,17 +1506,17 @@ Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed. (* Property localization *) -Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). -Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). -Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). -Notation Local ph := (phantom _). +Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). +Local Notation ph := (phantom _). Section LocalProperties. Variables T1 T2 T3 : Type. Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3). -Notation Local ph := (phantom Prop). +Local Notation ph := (phantom Prop). Definition prop_for (x : T1) P & ph {all1 P} := P x. diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v index c5a881f..f81e16e 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v +++ b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v @@ -1506,17 +1506,17 @@ Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed. (* Property localization *) -Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). -Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). -Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). -Notation Local ph := (phantom _). +Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). +Local Notation ph := (phantom _). Section LocalProperties. Variables T1 T2 T3 : Type. Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3). -Notation Local ph := (phantom Prop). +Local Notation ph := (phantom Prop). Definition prop_for (x : T1) P & ph {all1 P} := P x. |