diff options
| author | Hugo Herbelin | 2018-03-08 18:22:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 06fc6caa49b67526cf3521d1b5885aae6710358b (patch) | |
| tree | c893a474c67d9f569e1e19c7ccaedb1a02ada4f5 /test-suite | |
| parent | 74dfaaa8555f53bfc75216205823a8020e80b6a1 (diff) | |
Addressing issues with PR#873: performance and use of abbreviation for printing.
We do a couple of changes:
- Splitting notation keys into more categories to make table smaller.
This should (a priori) make printing faster (see #6416).
- Abbreviations are treated for printing like single notations: they
are pushed to the scope stack, so that in a situation such as
Open Scope foo_scope.
Notation foo := term.
Open Scope bar_scope.
one looks for notations first in scope bar_scope, then try to use
foo, they try for notations in scope foo_scope.
- We seize the opportunity of this commit to simplify
availability_of_notation which is now integrated to
uninterp_notation and which does not have to be called explicitly
anymore.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Inductive.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 6d65db9e22..5a548cfae4 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,6 +1,6 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in - "A -> list' A -> list' (A * A)%type". + "A -> list' A -> list' (A * A)". Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index e3816d65fd..bec4fc1579 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -64,7 +64,7 @@ The command has indeed failed with message: Cannot find where the recursive pattern starts. The command has indeed failed with message: Both ends of the recursive pattern are the same. -(nat * nat + nat)%type +SUM (nat * nat) nat : Set FST (0; 1) : Z diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 672a742f24..41d1593758 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -51,7 +51,7 @@ end match n with | nil => 2 | 0 :: _ => 2 -| 1 :: nil => 0 +| list1 => 0 | 1 :: _ :: _ => 2 | plus2 _ :: _ => 2 end |