diff options
| author | Georges Gonthier | 2019-04-29 11:12:26 +0200 |
|---|---|---|
| committer | Georges Gonthier | 2019-04-29 17:51:05 +0200 |
| commit | dae54440f08364552e1a82ac7984f35d1864f1e5 (patch) | |
| tree | ee443d2cf69970aece83d93435fe598994fbf8ff /mathcomp | |
| parent | 6be8fd5c67949a59bde7083e81401263986e7a4e (diff) | |
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.
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 3 |
1 files changed, 2 insertions, 1 deletions
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). |