From a89bde7b31393947c2c52e2dc75c61aa9cbf9e8e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Jul 2020 20:37:00 +0200
Subject: 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.
---
 test-suite/output/PrintAssumptions.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

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
-- 
cgit v1.2.3