From ba27c2e21f80b41dfd837e6c6b15f82ca405cf04 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 14 Feb 2018 02:06:02 +0100
Subject: [coq] Adapt to coq/coq#6511

coq/coq#6511 contains EConstr-related changes.
---
 src/tac2entries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index e48bf02321..fa498ab44f 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -344,7 +344,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
     in
     let () =
       if exists then
-        user_err ?loc (str "Tactic " ++ Nameops.pr_id id ++ str " already exists")
+        user_err ?loc (str "Tactic " ++ Names.Id.print id ++ str " already exists")
     in
     (id, e, t)
   in
@@ -539,7 +539,7 @@ let parse_scope = function
   if Id.Map.mem id !scope_table then
     Id.Map.find id !scope_table toks
   else
-    CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id)
+    CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id)
 | SexprStr (_, str) ->
   let v_unit = Loc.tag @@ CTacCst (AbsKn (Tuple 0)) in
   ScopeRule (Extend.Atoken (Tok.IDENT str), (fun _ -> v_unit))
-- 
cgit v1.2.3