diff options
| author | Cyril Cohen | 2020-03-25 18:56:56 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-04-06 12:40:23 +0200 |
| commit | a00523aee7c13fa5c2a2025ac2fe9412ad7ca5ee (patch) | |
| tree | 469594adf87504dc661967a3530afa564c02efc7 /mathcomp/ssreflect | |
| parent | a0d310fef7b4023793e74af103955e2dd8832faf (diff) | |
Some proof scripts made better using ssrAC.
%AC annotation are for backward compatilibity with coq <= 8.9
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/ssrAC.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/ssrAC.v b/mathcomp/ssreflect/ssrAC.v index 151e8ae..8483f71 100644 --- a/mathcomp/ssreflect/ssrAC.v +++ b/mathcomp/ssreflect/ssrAC.v @@ -227,9 +227,9 @@ Notation opAC op p s := (opACof op (AC.pattern p%AC) s%AC). Notation opACl op s := (opAC op (AC.Leaf_of_nat (size (AC.serial s%AC))) s%AC). Notation "op .[ 'ACof' p s ]" := (opACof op p s) - (at level 2, p at level 0, left associativity). + (at level 2, p at level 1, left associativity). Notation "op .[ 'AC' p s ]" := (opAC op p s) - (at level 2, p at level 0, left associativity). + (at level 2, p at level 1, left associativity). Notation "op .[ 'ACl' s ]" := (opACl op s) (at level 2, left associativity). |