aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2014-12-19 10:36:27 +0100
committerHugo Herbelin2014-12-19 11:40:16 +0100
commit5bbe23801d8961b04d54f48123f01b21e43261c3 (patch)
tree28116aded95c08218c78e80745763e6a4daea154
parentece8843f95a28c3ac123cda70c9a870a90a37b85 (diff)
Fixing wrong notation level in #3295.
-rw-r--r--test-suite/bugs/opened/3295.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v
index d871f5d20d..2a156e333a 100644
--- a/test-suite/bugs/opened/3295.v
+++ b/test-suite/bugs/opened/3295.v
@@ -50,7 +50,7 @@ Infix "==" := weq (at level 79).
Infix "*" := (dot _ _ _) (left associativity, at level 40).
Notation "āˆ‘_ ( i ∈ l ) f" := (@sup (mor _ _) _ (fun i => f) l)
- (at level 41, F at level 41, i, A at level 50).
+ (at level 41, f at level 41, i, l at level 50).
Axiom dotxsum : forall `{X : ops} I J n m p (f: I -> X m n) (x: X p m) y,
x * (āˆ‘_(i∈ J) f i) == y.