diff options
| author | Maxime Dénès | 2019-09-26 10:59:39 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-09-26 10:59:39 +0200 |
| commit | 884b413e91d293a6b2009da11f2996db0654e40f (patch) | |
| tree | eb9ca92acdea668507f31659a5609f5570ea5be2 /kernel/kernel.mllib | |
| parent | 59079a232d2157c0c4bea4cb1a3cd68c9410e880 (diff) | |
| parent | 6adc6e9484fde99ae943b31989f1454b6d079aaa (diff) | |
Merge PR #10664: Putting sections libstack inside the kernel
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/kernel.mllib')
| -rw-r--r-- | kernel/kernel.mllib | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 59c1d5890f..20e742d7f8 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,9 +43,11 @@ Inductive Typeops IndTyping Indtypes +InferCumulativity Cooking Term_typing Subtyping Mod_typing Nativelibrary +Section Safe_typing |