diff options
| author | Pierre-Marie Pédrot | 2016-04-08 15:03:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-08 15:22:53 +0200 |
| commit | 08c04d63f46e4b97c1055e8d066ad08229a484aa (patch) | |
| tree | b450c56ef3f4a7cd0520d07645ef8fd45d01345c /mathcomp/ssreflect/ssrbool.v | |
| parent | e9538e31be76c118f1e7aecb53fa89a94132fbdf (diff) | |
Fixing compilation after the merge of PR trunk-function_scope.
Diffstat (limited to 'mathcomp/ssreflect/ssrbool.v')
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index ee721d3..9049608 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -1604,6 +1604,8 @@ Notation "{ 'on' cd & , P }" := (prop_on2 (mem cd) (inPhantom P) (inPhantom P)) (at level 0, format "{ 'on' cd & , P }") : type_scope. +Local Arguments onPhantom {_%type_scope} _ _. + Notation "{ 'on' cd , P & g }" := (prop_on1 (mem cd) (Phantom (_ -> Prop) P) (onPhantom P g)) (at level 0, format "{ 'on' cd , P & g }") : type_scope. |