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` --- interp/syntax_def.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'interp/syntax_def.ml') diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 84c6f4ef3..98e507309 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -6,16 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CErrors open Util open Pp +open CErrors open Names open Libnames -open Notation_term open Libobject open Lib -open Nameops open Nametab +open Notation_term (* Syntactic definitions. *) @@ -31,7 +30,7 @@ let add_syntax_constant kn c onlyparse = let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if Nametab.exists_cci sp then user_err ~hdr:"cache_syntax_constant" - (pr_id (basename sp) ++ str " already exists"); + (Id.print (basename sp) ++ str " already exists"); add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn -- cgit v1.2.3