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/cbytegen.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/cbytegen.ml') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index d63fcffa2..5bac26bf9 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -998,7 +998,7 @@ let compile_constant_body fail_on_error env univs = function match kind_of_term body with | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) - let con= constant_of_kn (canonical_con kn') in + let con= Constant.make1 (Constant.canonical kn') in Some (BCalias (get_alias env con)) | _ -> let res = compile fail_on_error ~universes:instance_size env body in @@ -1006,7 +1006,7 @@ let compile_constant_body fail_on_error env univs = function (* Shortcut of the previous function used during module strengthening *) -let compile_alias kn = BCalias (constant_of_kn (canonical_con kn)) +let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn)) (* spiwack: additional function which allow different part of compilation of the 31-bit integers *) -- cgit v1.2.3