From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 printing/prettyp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 797b6faa08..8bf86e9ef6 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -505,9 +505,9 @@ let gallina_print_named_decl env sigma =
   let open Context.Named.Declaration in
   function
   | LocalAssum (id, typ) ->
-     print_named_assum env sigma (Id.to_string id) typ
+     print_named_assum env sigma (Id.to_string id.Context.binder_name) typ
   | LocalDef (id, body, typ) ->
-     print_named_def env sigma (Id.to_string id) body typ
+     print_named_def env sigma (Id.to_string id.Context.binder_name) body typ
 
 let assumptions_for_print lna =
   List.fold_right (fun na env -> add_name na env) lna empty_names_context
-- 
cgit v1.2.3