diff options
| author | Enrico | 2016-04-15 15:30:45 +0200 |
|---|---|---|
| committer | Enrico | 2016-04-15 15:30:45 +0200 |
| commit | 374222f28aea5f8cdce246fb9e7b68b612a4349e (patch) | |
| tree | b450c56ef3f4a7cd0520d07645ef8fd45d01345c | |
| parent | e9538e31be76c118f1e7aecb53fa89a94132fbdf (diff) | |
| parent | 08c04d63f46e4b97c1055e8d066ad08229a484aa (diff) | |
Merge pull request #39 from ppedrot/partial-fix
Fixing compilation after the merge of PR trunk-function_scope.
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 2 |
2 files changed, 4 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. diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 1ff82ab..a271eb2 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -184,6 +184,8 @@ End TheCanonical. Import TheCanonical. (* Note: no export. *) +Local Arguments get_by _%type_scope _%type_scope _ _ _ _. + Notation "[ 'the' sT 'of' v 'by' f ]" := (@get_by _ sT f _ _ ((fun v' (s : sT) => Put v' (f s) s) v _)) (at level 0, only parsing) : form_scope. |