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 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/printer.ml')

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