blob: 247155d8b3f1db5b00af404168cd0f0565d7f827 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* This was failing at parsing *)
Notation "'a'" := tt (only printing).
Goal True. let a := constr:(1+1) in idtac a. Abort.
(* Idem *)
Require Import Coq.Strings.String.
Require Import Coq.ZArith.ZArith.
Open Scope string_scope.
Axiom Ox: string -> Z.
Axiom isMMIOAddr: Z -> Prop.
Notation "'Ox' a" := (Ox a) (only printing, at level 10, format "'Ox' a").
Goal False.
set (f := isMMIOAddr).
set (x := f (Ox "0018")).
Abort.
|
