Adapt universe polymorphic branch to new handling of futures for delayed proofs.

8 files changed, 21 insertions, 23 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7fbf2f5ac..97445755f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -64,7 +64,7 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       let () = Global.push_named_def (id,de) in
         Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
-	(Univ.ContextSet.of_context (Future.force de.const_entry_universes)) in
+	(Univ.ContextSet.of_context de.const_entry_universes) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -126,7 +126,7 @@ let open_constant i ((sp,kn), obj) =
     | (Def _ | Undef _) -> ()
     | OpaqueDef lc ->
         match Opaqueproof.get_constraints lc with
-        | Some f when Future.is_val f -> Global.add_constraints (Future.force f)
+        | Some f when Future.is_val f -> Global.push_context (Future.force f)
         | _ -> ()
 
 let exists_name id =
@@ -201,7 +201,7 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
     const_entry_type = types;
     const_entry_proj = None;
     const_entry_polymorphic = poly;
-    const_entry_universes = Future.from_val univs;
+    const_entry_universes = univs;
     const_entry_opaque = opaque;
     const_entry_feedback = None;
     const_entry_inline_code = inline}
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 5ff471e69..a25247891 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -73,7 +73,7 @@ type library_objects
 val register_library :
   library_name ->
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
-  Univ.constraints -> unit
+  Univ.universe_context -> unit
 
 val get_library_symbols_tbl : library_name -> Nativecode.symbol array
 
diff --git a/library/global.ml b/library/global.ml
index 812178bbb..74a2a1c0e 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -172,10 +172,8 @@ let type_of_global_in_context env r =
   | VarRef id -> Environ.named_type id env, Univ.UContext.empty
   | ConstRef c -> 
      let cb = Environ.lookup_constant c env in 
-     let univs = 
-       if cb.const_polymorphic then Future.force cb.const_universes 
-       else Univ.UContext.empty
-     in Typeops.type_of_constant_type env cb.Declarations.const_type, univs
+     let univs = Declareops.universes_of_polymorphic_constant cb in
+       Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
      let univs = 
diff --git a/library/global.mli b/library/global.mli
index 410be961b..5995ff03f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -94,7 +94,7 @@ val start_library : DirPath.t -> module_path
 val export : DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
-  Safe_typing.compiled_library -> Univ.constraints -> Safe_typing.vodigest ->
+  Safe_typing.compiled_library -> Univ.universe_context -> Safe_typing.vodigest ->
   module_path * Nativecode.symbol array
 
 (** {6 Misc } *)
diff --git a/library/library.ml b/library/library.ml
index 8521325b0..dc712ce02 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -39,7 +39,7 @@ type library_t = {
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
   library_digests : Safe_typing.vodigest;
-  library_extra_univs : Univ.constraints;
+  library_extra_univs : Univ.universe_context;
 }
 
 module LibraryOrdered = DirPath
@@ -329,7 +329,7 @@ type 'a table_status =
 let opaque_tables =
   ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
 let univ_tables =
-  ref (LibraryMap.empty : (Univ.constraints table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Univ.universe_context table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -354,7 +354,7 @@ let access_opaque_table dp i =
     add_opaque_table !opaque_tables dp i
 let access_univ_table dp i =
   access_table
-    (fetch_table "universe constraints of opaque proofs")
+    (fetch_table "universe contexts of opaque proofs")
     add_univ_table !univ_tables dp i
 
 (** Table of opaque terms from the library currently being compiled *)
@@ -362,7 +362,7 @@ let access_univ_table dp i =
 module OpaqueTables = struct
 
  let a_constr = Future.from_val (Term.mkRel 1)
- let a_univ = Future.from_val Univ.empty_constraint
+ let a_univ = Future.from_val Univ.UContext.empty
  let a_discharge : Opaqueproof.cooking_info list = []
 
  let local_opaque_table = ref (Array.make 100 a_constr)
@@ -440,7 +440,7 @@ let () =
 
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.constraints Future.computation array * Univ.constraints * bool
+  Univ.universe_context Future.computation array * Univ.universe_context * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
@@ -466,13 +466,13 @@ let intern_from_file f =
   add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
   let open Safe_typing in
   match univs with
-  | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint
+  | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty
   | Some (utab,uall,true) ->
       add_univ_table lmd.md_name (Fetched utab);
       mk_library lmd (Dvivo (digest_lmd,digest_u)) uall
   | Some (utab,_,false) ->
       add_univ_table lmd.md_name (Fetched utab);
-      mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint
+      mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty
 
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
@@ -731,7 +731,7 @@ let save_library_to ?todo dir f =
     | Some d ->
         assert(!Flags.compilation_mode = Flags.BuildVi);
         f ^ "i", (fun x -> Some (d x)),
-          (fun x -> Some (x,Univ.empty_constraint,false)), (fun x -> Some x) in
+          (fun x -> Some (x,Univ.UContext.empty,false)), (fun x -> Some x) in
   Opaqueproof.reset_indirect_creator ();
   let cenv, seg, ast = Declaremods.end_library dir in
   let opaque_table, univ_table, disch_table, f2t_map =
diff --git a/library/library.mli b/library/library.mli
index 16664d880..fc043aab6 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -31,7 +31,7 @@ val require_library_from_file :
 (** Segments of a library *)
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
-  Univ.constraints Future.computation array * Univ.constraints * bool
+  Univ.universe_context Future.computation array * Univ.universe_context * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
diff --git a/library/universes.ml b/library/universes.ml
index 2b42e3fe8..138a248f0 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -63,7 +63,7 @@ let unsafe_instance_from ctx =
 let fresh_constant_instance env c =
   let cb = lookup_constant c env in
     if cb.Declarations.const_polymorphic then
-      let (inst,_), ctx = fresh_instance_from (Future.force cb.Declarations.const_universes) in
+      let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in
 	((c, inst), ctx)
     else ((c,Instance.empty), ContextSet.empty)
 
@@ -84,7 +84,7 @@ let fresh_constructor_instance env (ind,i) =
 let unsafe_constant_instance env c =
   let cb = lookup_constant c env in
     if cb.Declarations.const_polymorphic then
-      let inst, ctx = unsafe_instance_from (Future.force cb.Declarations.const_universes) in
+      let inst, ctx = unsafe_instance_from (Declareops.universes_of_constant cb) in
 	((c, inst), ctx)
     else ((c,Instance.empty), UContext.empty)
 
@@ -183,7 +183,7 @@ let type_of_reference env r =
      let cb = Environ.lookup_constant c env in
      let ty = Typeops.type_of_constant_type env cb.const_type in
        if cb.const_polymorphic then
-	 let (inst, subst), ctx = fresh_instance_from (Future.force cb.const_universes) in
+	 let (inst, subst), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in
 	   Vars.subst_univs_constr subst ty, ctx
        else ty, ContextSet.empty
 
@@ -676,7 +676,7 @@ let restrict_universe_context (univs,csts) s =
       csts Constraint.empty
   in (univs', csts')
 
-let simplify_universe_context (univs,csts) s =
+let simplify_universe_context (univs,csts) =
   let uf = UF.create () in
   let noneqs =
     Constraint.fold (fun (l,d,r) noneqs ->
diff --git a/library/universes.mli b/library/universes.mli
index 150686d73..ab217e872 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -171,7 +171,7 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
 val universes_of_constr : constr -> universe_set
 val shrink_universe_context : universe_context_set -> universe_set -> universe_context_set
 val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
-val simplify_universe_context : universe_context_set -> universe_set -> 
+val simplify_universe_context : universe_context_set -> 
   universe_context_set * universe_level_subst
 
 val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes