From c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 13 Nov 2017 18:43:02 +0100
Subject: [api] Another large deprecation, `Nameops`

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

(limited to 'vernac/auto_ind_decl.ml')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 3cf181441..9e63df51d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -19,7 +19,6 @@ open Termops
 open Declarations
 open Names
 open Globnames
-open Nameops
 open Inductiveops
 open Tactics
 open Ind_tables
@@ -361,7 +360,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
             else user_err ~hdr:"AutoIndDecl.do_replace_lb"
-                   (str "Var " ++ pr_id s ++ str " seems unknown.")
+                   (str "Var " ++ Id.print s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when CErrors.noncritical e ->
@@ -422,7 +421,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
             else user_err ~hdr:"AutoIndDecl.do_replace_bl"
-                   (str "Var " ++ pr_id s ++ str " seems unknown.")
+                   (str "Var " ++ Id.print s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when CErrors.noncritical e ->
-- 
cgit v1.2.3