From c3e26fca1d077a2b69926df85d05e067882c40b0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 19 Dec 2017 08:33:55 +0100
Subject: Specific type for section definition entries.

This allows to statically ensure well-formedness properties.
---
 interp/declare.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 8781c87192..ae28c4b90e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -231,7 +231,15 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       let (de, eff) = Global.export_private_constants ~in_section:true de in
       let () = List.iter register_side_effect eff in
-      let univs = Global.push_named_def (id,de) in
+      let body = Future.chain de.const_entry_body (fun (body, ()) -> body) in
+      let se = {
+        secdef_body = body;
+        secdef_secctx = de.const_entry_secctx;
+        secdef_universes = de.const_entry_universes;
+        secdef_feedback = de.const_entry_feedback;
+        secdef_type = de.const_entry_type;
+      } in
+      let univs = Global.push_named_def (id, se) in
       let poly = match de.const_entry_universes with
       | Monomorphic_const_entry _ -> false
       | Polymorphic_const_entry _ -> true
-- 
cgit v1.2.3