diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-16 22:17:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-17 08:02:45 +0100 |
| commit | 9f5586d88880cbb98c92edfe9c33c76564f1a19c (patch) | |
| tree | 6de2a171eff5706b0e4ce9268554b84a922f12b3 /kernel/nativeinstr.mli | |
| parent | 4985f0ff99278beb3b934f86edf1398659c611a8 (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 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 |