diff options
| author | Maxime Dénès | 2015-01-16 22:17:03 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:43 +0530 |
| commit | 6e0b660b1e58502b7da477b9725ae8ee4f5d00ed (patch) | |
| tree | 36114b255b884e90b021876bebd49ff978c24710 /kernel/nativeinstr.mli | |
| parent | a83721ac508aa96496ef95c8433bc282bca0db14 (diff) | |
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.
Diffstat (limited to 'kernel/nativeinstr.mli')
| -rw-r--r-- | kernel/nativeinstr.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index ad541ad73c..b7d3dadcd8 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 |