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
---
 printing/printer.ml                    | 4 ++--
 test-suite/output/Implicit.out         | 2 +-
 test-suite/output/NumeralNotations.out | 2 +-
 test-suite/output/NumeralNotations.v   | 1 +
 vernac/prettyp.ml                      | 6 +++---
 5 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index bb54f587fd..18d6bcb3f1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -281,7 +281,7 @@ let pr_compacted_decl env sigma decl =
        ids, mt (), typ
     | CompactedDecl.LocalDef (ids,c,typ) ->
        (* Force evaluation *)
-       let pb = pr_lconstr_env env sigma c in
+       let pb = pr_lconstr_env ~inctx:true env sigma c in
        let pb = if isCast c then surround pb else pb in
        ids, (str" := " ++ pb ++ cut ()), typ
   in
@@ -300,7 +300,7 @@ let pr_rel_decl env sigma decl =
     | RelDecl.LocalAssum _ -> mt ()
     | RelDecl.LocalDef (_,c,_) ->
         (* Force evaluation *)
-        let pb = pr_lconstr_env env sigma c in
+        let pb = pr_lconstr_env ~inctx:true env sigma c in
         let pb = if isCast c then surround pb else pb in
         (str":=" ++ spc () ++ pb ++ spc ()) in
   let ptyp = pr_ltype_env env sigma typ in
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 *)
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ea49cae9db..fdf999b5b8 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -545,7 +545,7 @@ let print_located_qualid ref = print_located_qualid "object" LocAny ref
 (****  Gallina layer                  *****)
 
 let gallina_print_typed_value_in_env env sigma (trm,typ) =
-  (pr_leconstr_env env sigma trm ++ fnl () ++
+  (pr_leconstr_env ~inctx:true env sigma trm ++ fnl () ++
      str "     : " ++ pr_letype_env env sigma typ)
 
 (* To be improved; the type should be used to provide the types in the
@@ -554,7 +554,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) =
    synthesizes the type nat of the abstraction on u *)
 
 let print_named_def env sigma name body typ =
-  let pbody = pr_lconstr_env env sigma body in
+  let pbody = pr_lconstr_env ~inctx:true env sigma body in
   let ptyp = pr_ltype_env env sigma typ in
   let pbody = if Constr.isCast body then surround pbody else pbody in
   (str "*** [" ++ str name ++ str " " ++
@@ -596,7 +596,7 @@ let gallina_print_section_variable env sigma id =
   with_line_skip (print_name_infos (GlobRef.VarRef id))
 
 let print_body env evd = function
-  | Some c  -> pr_lconstr_env env evd c
+  | Some c  -> pr_lconstr_env ~inctx:true env evd c
   | None -> (str"<no body>")
 
 let print_typed_body env evd (val_0,typ) =
-- 
cgit v1.2.3