From a00523aee7c13fa5c2a2025ac2fe9412ad7ca5ee Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 25 Mar 2020 18:56:56 +0100 Subject: Some proof scripts made better using ssrAC. %AC annotation are for backward compatilibity with coq <= 8.9 --- mathcomp/ssreflect/ssrAC.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/ssreflect') 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). -- cgit v1.2.3