diff options
| author | Emilio Jesus Gallego Arias | 2020-02-19 15:56:50 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-19 15:56:50 -0500 |
| commit | a644482acd84427db0e64450c3fc41ad321e83cd (patch) | |
| tree | bac186931ae4170d1f1b0e3c043be95ebbc8e243 /test-suite | |
| parent | 2b72b403d82c15d0420603142e14ab50c7e590c1 (diff) | |
| parent | 25cab58df1171c9419396342e9ecc3094b74eca5 (diff) | |
Merge PR #11636: Revert buggy commit mistakenly pushed with #11530
Reviewed-by: ejgallego
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. |