From 64e66fd019b968f863a80d4bce972545a66ea966 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jun 2019 19:05:06 +0200
Subject: Perform the opaque section variable inference outside of the kernel.

It is not the role of the kernel to decide to force the body of an entry
to infer the section variable it uses, but the one of the upper layers.
We make this explicit in the type of entries so as to enforce that this
inference is performed beforehand.

Also removes auxilliary file stuff that doesn't look like it belongs in
the kernel either.
---
 kernel/entries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 2d29c3ee19..ca08ba485e 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -80,7 +80,7 @@ type section_def_entry = {
 type 'a opaque_entry = {
   opaque_entry_body   : 'a;
   (* List of section variables *)
-  opaque_entry_secctx : Constr.named_context option;
+  opaque_entry_secctx : Constr.named_context;
   (* State id on which the completion of type checking is reported *)
   opaque_entry_feedback : Stateid.t option;
   opaque_entry_type        : types;
-- 
cgit v1.2.3