From 8860362de4a26286b0cb20cf4e02edc5209bdbd1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 23:35:51 +0200
Subject: Univs: Change intf of push_named_def to return the computed universe
 context

Let-bound definitions can be opaque but the whole universe context
was not gathered to be discharged at section closing time.
---
 kernel/safe_typing.ml  | 17 +++++++++--------
 kernel/safe_typing.mli |  5 ++++-
 2 files changed, 13 insertions(+), 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4299f729da..9329b16861 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -338,17 +338,18 @@ let safe_push_named (id,_,_ as d) env =
 
 let push_named_def (id,de) senv =
   let c,typ,univs = Term_typing.translate_local_def senv.env id de in
-  let senv' = push_context de.Entries.const_entry_polymorphic univs senv in
-  let c, senv' = match c with
-    | Def c -> Mod_subst.force_constr c, senv'
+  let poly = de.Entries.const_entry_polymorphic in
+  let univs = Univ.ContextSet.of_context univs in
+  let c, univs = match c with
+    | Def c -> Mod_subst.force_constr c, univs
     | OpaqueDef o ->
-        Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
-        push_context_set de.Entries.const_entry_polymorphic
-	 (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
-          senv'
+        Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
+        Univ.ContextSet.union univs 
+	(Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
     | _ -> assert false in
+  let senv' = push_context_set poly univs senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
-    {senv' with env=env''}
+    univs, {senv' with env=env''}
 
 let push_named_assum ((id,t,poly),ctx) senv =
   let senv' = push_context_set poly ctx senv in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b971a1bd42..eac08eb834 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -59,8 +59,11 @@ val is_joined_environment : safe_environment -> bool
 val push_named_assum :
   (Id.t * Term.types * bool (* polymorphic *))
     Univ.in_universe_context_set -> safe_transformer0
+
+(** Returns the full universe context necessary to typecheck the definition
+  (futures are forced) *)
 val push_named_def :
-  Id.t * Entries.definition_entry -> safe_transformer0
+  Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
-- 
cgit v1.2.3