From d696eb98189eccdc2f6adb851e54af37e7f8d83b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Nov 2019 16:27:15 +0100
Subject: When printing term together with its type, use info that term is in
 context.

This governs the printing of the explicitation of implicit arguments
and the removal of coercions.

E.g., "Check coe foo." where coe is a coercion with codomain B will show:

foo
    : B

instead of

coe foo
    : B
---
 test-suite/output/Implicit.out         | 2 +-
 test-suite/output/NumeralNotations.out | 2 +-
 test-suite/output/NumeralNotations.v   | 1 +
 3 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 5f22eb5d7c..28afd06fbc 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -1,4 +1,4 @@
-compose (C:=nat) S
+compose S
      : (nat -> nat) -> nat -> nat
 ex_intro (P:=fun _ : nat => True) (x:=0) I
      : ex (fun _ : nat => True)
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 505dc52ebe..113384e9cf 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -75,7 +75,7 @@ The command has indeed failed with message:
 In environment
 v := 0 : nat
 The term "v" has type "nat" while it is expected to have type "wuint".
-File "stdin", line 202, characters 2-72:
+File "stdin", line 203, characters 2-72:
 Warning: The 'abstract after' directive has no effect when the parsing
 function (of_uint) targets an option type.
 [abstract-large-number-no-op,numbers]
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index c306b15ef3..22aff36d67 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -123,6 +123,7 @@ Module Test6.
     Export Scopes.
     Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000).
   End Notations.
+  Set Printing Coercions.
   Check let v := 0%wnat in v : wnat.
   Check wrap O.
   Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *)
-- 
cgit v1.2.3