Merge PR #11143: In Print/Check/Show, adopt the view that the attached type information may impact the display of coercion and implicit arguments.

Reviewed-by: ejgallego

5 files changed, 8 insertions, 7 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index cc83a1dde0..b376616b61 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -278,7 +278,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
@@ -297,7 +297,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 32c438c724..cdd93db884 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -547,7 +547,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
@@ -556,7 +556,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 " " ++
@@ -598,7 +598,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) =