diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /kernel/nativeinstr.mli | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
Diffstat (limited to 'kernel/nativeinstr.mli')
| -rw-r--r-- | kernel/nativeinstr.mli | 14 |
1 files changed, 7 insertions, 7 deletions
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 |