From e29948c5606bfcab182cf0f325750fdb3215856e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 4 Jul 2017 19:37:07 +0200
Subject: An occurrence of set_id which behaves as the identity.

---
 printing/prettyp.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2077526db4..fdaeded878 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -807,7 +807,8 @@ let print_any_name = function
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
     if not (DirPath.is_empty dir) then raise Not_found;
-    str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl
+    str |> Global.lookup_named |> print_named_decl
+
   with Not_found ->
     user_err
       ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
@@ -839,7 +840,7 @@ let print_opaque_name qid =
         let open EConstr in
 	print_typed_value (mkConstruct cstr, ty)
     | VarRef id ->
-        env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
+        env |> lookup_named id |> print_named_decl
 
 let print_about_any ?loc k =
   match k with
-- 
cgit v1.2.3