From 9f5586d88880cbb98c92edfe9c33c76564f1a19c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Jan 2015 22:17:03 +0100 Subject: Make native compiler handle universe polymorphic definitions. One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem. --- kernel/nativeinstr.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/nativeinstr.mli') diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index ad541ad73..b7d3dadcd 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -28,7 +28,7 @@ and lambda = | Llam of name array * lambda | Llet of name * lambda * lambda | Lapp of lambda * lambda array - | Lconst of prefix * constant + | Lconst of prefix * pconstant | Lproj of prefix * constant (* prefix, projection name *) | Lprim of prefix * constant * Primitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches @@ -36,15 +36,15 @@ and lambda = | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl - | Lmakeblock of prefix * constructor * int * lambda array + | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) - | Lconstruct of prefix * constructor + | Lconstruct of prefix * pconstructor (* A partially applied constructor *) | Luint of uint | Lval of Nativevalues.t | Lsort of sorts - | Lind of prefix * inductive + | Lind of prefix * pinductive | Llazy | Lforce -- cgit v1.2.3