diff options
| author | Pierre-Marie Pédrot | 2019-03-04 15:16:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 13:59:40 +0100 |
| commit | 6632739f853e42e5828fbf603f7a3089a00f33f7 (patch) | |
| tree | deb37273d04b10af35d55b191484269f9b5443f7 | |
| parent | a22da3e70551658deefbbedf261acdc3ead5403d (diff) | |
Move the relative linking order of Inductive w.r.t. VM / native.
We need this file for the upcoming kernel representation change there.
| -rw-r--r-- | kernel/kernel.mllib | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 5b2a7bd9c2..75fd70d923 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -31,6 +31,8 @@ Primred CClosure Relevanceops Reduction +Type_errors +Inductive Vmlambda Nativelambda Vmbytegen @@ -40,9 +42,7 @@ Vmsymtable Vm Vconv Nativeconv -Type_errors Modops -Inductive Typeops InferCumulativity IndTyping |