diff options
| author | Hugo Herbelin | 2020-07-12 20:37:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-15 21:48:25 +0200 |
| commit | a89bde7b31393947c2c52e2dc75c61aa9cbf9e8e (patch) | |
| tree | 4fccdec595b66741023dc88c040a10446e7031e9 /test-suite | |
| parent | 33e748514dad9459885006a1523d107d556be22b (diff) | |
Do not print global refs as terms when asked to be printed as themselves.
This was already the case for constant, but not for constructors and
inductive types.
For instance, in message "The constructor @cons (in type list) is
expected to ..." we don't want a @ to be printed.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ba316ceb64..b8db52735d 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,7 +7,7 @@ bli : Type Axioms: bli : Type Axioms: -@seq relies on definitional UIP. +seq relies on definitional UIP. Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g |