From dae54440f08364552e1a82ac7984f35d1864f1e5 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Mon, 29 Apr 2019 11:12:26 +0200
Subject: reinstate token catenation hack in `prime.v`

Appears to be needed fo v8.7 compatibility, to avert some bug in early
`only printing` implementation whose fix was not back ported.
---
 mathcomp/ssreflect/prime.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index bfecfa9..bcb163c 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -162,7 +162,8 @@ Definition pi_of (n : pi_arg) : nat_pred := [pred p in primes n].
 
 Notation "\pi ( n )" := (pi_of n)
   (at level 2, format "\pi ( n )") : nat_scope.
-Notation "\pi ( A )" := \pi(#|A|) (only printing) : nat_scope.
+Notation "\p 'i' ( A )" := \pi(#|A|) 
+  (at level 2, format "\p 'i' ( A )") : nat_scope.
 
 Definition pdiv n := head 1 (primes n).
 
-- 
cgit v1.2.3