diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 3 |
2 files changed, 0 insertions, 5 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 1c8f237bb8..807914a671 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,8 +14,6 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat -[2 + 3] - : nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4ab800c9ba..2906698386 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,9 +22,6 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). Check [ << # 0 >> ]. -Notation "n" := n%nat (in custom myconstr at level 0, n bigint). -Check [ 2 + 3 ]. - End A. Module B. |