From 08c04d63f46e4b97c1055e8d066ad08229a484aa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 8 Apr 2016 15:03:53 +0200
Subject: Fixing compilation after the merge of PR trunk-function_scope.

---
 mathcomp/ssreflect/ssrbool.v   | 2 ++
 mathcomp/ssreflect/ssreflect.v | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'mathcomp')

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.
-- 
cgit v1.2.3