From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- kernel/declareops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 66d66c7d0..d7329a319 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -287,9 +287,9 @@ let hcons_mind mib = (** {6 Stm machinery } *) let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" (** Hashconsing of modules *) -- cgit v1.2.3