Fixing compilation after the merge of PR trunk-function_scope.

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.