From c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Nov 2017 18:43:02 +0100 Subject: [api] Another large deprecation, `Nameops` --- vernac/declareDef.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index d7a4fcca3..c18744052 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -11,18 +11,17 @@ open Declare open Entries open Globnames open Impargs -open Nameops let warn_definition_not_visible = CWarnings.create ~name:"definition-not-visible" ~category:"implicits" Pp.(fun ident -> strbrk "Section definition " ++ - pr_id ident ++ strbrk " is not visible from current goals") + Names.Id.print ident ++ strbrk " is not visible from current goals") let warn_local_declaration = CWarnings.create ~name:"local-declaration" ~category:"scope" Pp.(fun (id,kind) -> - pr_id id ++ strbrk " is declared as a local " ++ str kind) + Names.Id.print id ++ strbrk " is declared as a local " ++ str kind) let get_locality id ~kind = function | Discharge -> -- cgit v1.2.3