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/nativeinstr.mli | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'kernel/nativeinstr.mli') diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 73f18f7a7..b2c8662da 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -20,17 +20,17 @@ type uint = | UintDecomp of prefix * constructor * lambda and lambda = - | Lrel of name * int + | Lrel of Name.t * int | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) | Levar of existential * lambda (* type *) | Lprod of lambda * lambda - | Llam of name array * lambda - | Llet of name * lambda * lambda + | Llam of Name.t array * lambda + | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * constant (* prefix, projection name *) - | Lprim of prefix * constant * CPrimitives.t * lambda array + | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda @@ -48,6 +48,6 @@ and lambda = | Llazy | Lforce -and lam_branches = (constructor * name array * lambda) array +and lam_branches = (constructor * Name.t array * lambda) array -and fix_decl = name array * lambda array * lambda array +and fix_decl = Name.t array * lambda array * lambda array -- cgit v1.2.3