diff options
| author | Hugo Herbelin | 2018-10-31 00:12:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-31 11:22:56 +0100 |
| commit | 2a38552ad35cdcd827da014106aa5b4af88dfb9e (patch) | |
| tree | e415d01370fc0c53c8cc68ade2e01cf5ed13207a /test-suite | |
| parent | 310f8fa900bc0d25a05f6409d941708a74aca60b (diff) | |
Notations: fixing a bug with abbreviations in custom entries.
Coercions were missing.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index cef7d1a702..46784d1897 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,7 @@ [< 0 > + < 1 > * < 2 >] : nat +[< b > + < b > * < 2 >] + : nat [<< # 0 >>] : option nat [1 {f 1}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 9738ce5a5e..6bdbf1bed5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Axiom a : nat. +Notation b := a. +Check [ < b > + < a > * < 2 >]. + Declare Custom Entry anotherconstr. Notation "[ x ]" := x (x custom myconstr at level 6). |