From 62fb849cf9410ddc2d9f355570f4fb859f3044c3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Tue, 25 Mar 2014 18:29:28 +0100
Subject: Adapt universe polymorphic branch to new handling of futures for
 delayed proofs.

---
 kernel/cooking.ml           |   2 +-
 kernel/declarations.mli     |   2 +-
 kernel/declareops.ml        |  20 ++--
 kernel/declareops.mli       |   6 ++
 kernel/entries.mli          |   2 +-
 kernel/environ.ml           |   8 +-
 kernel/mod_typing.ml        |   9 +-
 kernel/opaqueproof.ml       |   4 +-
 kernel/opaqueproof.mli      |   8 +-
 kernel/safe_typing.ml       |  22 +++--
 kernel/safe_typing.mli      |   2 +-
 kernel/subtyping.ml         |   4 +-
 kernel/term_typing.ml       |  17 ++--
 library/declare.ml          |   6 +-
 library/declaremods.mli     |   2 +-
 library/global.ml           |   6 +-
 library/global.mli          |   2 +-
 library/library.ml          |  16 ++--
 library/library.mli         |   2 +-
 library/universes.ml        |   8 +-
 library/universes.mli       |   2 +-
 plugins/funind/indfun.ml    |   1 -
 plugins/funind/invfun.ml    |   2 +-
 pretyping/typeclasses.ml    |   2 +-
 printing/prettyp.ml         |   5 +-
 proofs/pfedit.ml            |   4 +-
 proofs/pfedit.mli           |   4 +-
 proofs/proof_global.ml      |  99 +++++++++-----------
 proofs/proof_global.mli     |   8 +-
 proofs/proofview_monad.ml   | 217 +-------------------------------------------
 stm/lemmas.ml               |   2 +-
 stm/stm.ml                  |   6 +-
 theories/Logic/EqdepFacts.v |   2 +-
 toplevel/ind_tables.ml      |   2 +-
 toplevel/indschemes.ml      |   2 +-
 toplevel/obligations.ml     |   6 +-
 toplevel/record.ml          |   2 +-
 37 files changed, 148 insertions(+), 366 deletions(-)

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3d580d713..5fa01e5db 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -213,7 +213,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
       { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
 	proj_type = ty'; proj_body = c' }
   in
-  let univs = Future.from_val (UContext.union abs_ctx (Future.force cb.const_universes)) in
+  let univs = UContext.union abs_ctx cb.const_universes in
     (body, typ, Option.map projection cb.const_proj, 
      cb.const_polymorphic, univs, cb.const_inline_code, 
      Some const_hyps)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 9c7344f89..b8dfe63d3 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -61,7 +61,7 @@ type constant_def =
   | Def of constr Mod_subst.substituted
   | OpaqueDef of Opaqueproof.opaque
 
-type constant_universes = Univ.universe_context Future.computation
+type constant_universes = Univ.universe_context
 
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 8806bba45..4363ec442 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -43,11 +43,20 @@ let body_of_constant cb = match cb.const_body with
   | OpaqueDef o -> Some (Opaqueproof.force_proof o)
 
 let constraints_of_constant cb = Univ.Constraint.union 
-  (Univ.UContext.constraints (Future.force cb.const_universes))
+  (Univ.UContext.constraints cb.const_universes)
   (match cb.const_body with
   | Undef _ -> Univ.empty_constraint
   | Def c -> Univ.empty_constraint
-  | OpaqueDef o -> Opaqueproof.force_constraints o)
+  | OpaqueDef o -> Univ.UContext.constraints (Opaqueproof.force_constraints o))
+
+let universes_of_constant cb = 
+  match cb.const_body with
+  | Undef _ | Def _ -> cb.const_universes
+  | OpaqueDef o -> Opaqueproof.force_constraints o
+
+let universes_of_polymorphic_constant cb = 
+  if cb.const_polymorphic then universes_of_constant cb
+  else Univ.UContext.empty
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
@@ -139,11 +148,7 @@ let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = hcons_const_type cb.const_type;
-    const_universes =
-      if Future.is_val cb.const_universes then
-        Future.from_val
-          (Univ.hcons_universe_context (Future.force cb.const_universes))
-      else (* FIXME: Why not? *) cb.const_universes }
+    const_universes = Univ.hcons_universe_context cb.const_universes }
 
 (** {6 Inductive types } *)
 
@@ -265,7 +270,6 @@ let hcons_mind mib =
 (** {6 Stm machinery } *)
 
 let join_constant_body cb =
-  ignore(Future.join cb.const_universes);
   match cb.const_body with
   | OpaqueDef o -> Opaqueproof.join_opaque o
   | _ -> ()
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 9f5197668..6c43bffa9 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -30,6 +30,12 @@ val constant_has_body : constant_body -> bool
 
 val body_of_constant : constant_body -> Term.constr option
 val constraints_of_constant : constant_body -> Univ.constraints
+val universes_of_constant : constant_body -> Univ.universe_context
+
+(** Return the universe context, in case the definition is polymorphic, otherwise
+    the context is empty. *)
+
+val universes_of_polymorphic_constant : constant_body -> Univ.universe_context
 
 val is_opaque : constant_body -> bool
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index a161a6fcb..001a1e4b3 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -63,7 +63,7 @@ type definition_entry = {
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
   const_entry_polymorphic : bool;
-  const_entry_universes   : Univ.universe_context Future.computation;
+  const_entry_universes   : Univ.universe_context;
   const_entry_proj        : projection option;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ede655702..dd4237b22 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -207,7 +207,7 @@ let add_constant kn cb env =
   add_constant_key kn cb (no_link_info ()) env
 
 let universes_of cb = 
-  Future.force cb.const_universes
+  cb.const_universes
 
 let universes_and_subst_of cb u =
   let univs = universes_of cb in
@@ -234,7 +234,7 @@ let constant_type env (kn,u) =
 
 let constant_context env kn =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then Future.force cb.const_universes
+    if cb.const_polymorphic then cb.const_universes
     else Univ.UContext.empty
 
 type const_evaluation_result = NoBody | Opaque | IsProj
@@ -283,7 +283,7 @@ let constant_value_and_type env (kn, u) =
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
-      let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in
+      let subst = Univ.make_universe_subst u cb.const_universes in
 	map_regular_arity (subst_univs_constr subst) cb.const_type
     else cb.const_type
 
@@ -293,7 +293,7 @@ let constant_value_in env (kn,u) =
     | Def l_body -> 
       let b = Mod_subst.force_constr l_body in
 	if cb.const_polymorphic then
-	  let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in
+	  let subst = Univ.make_universe_subst u cb.const_universes in
 	    subst_univs_constr subst b
 	else b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b20fe9671..cab3276c3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,8 +72,8 @@ let rec check_with_def env struc (idl,c) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let env' = Environ.add_constraints 
-	(Univ.UContext.constraints (Future.force cb.const_universes)) env' in
+      let ccst = Declareops.constraints_of_constant cb in
+      let env' = Environ.add_constraints ccst env' in
       let c',cst = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
 	  let j = Typeops.infer env' c in
@@ -84,10 +84,9 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	| Def cs ->
 	  let cst = Reduction.infer_conv env' (Environ.universes env') c
 	    (Mod_subst.force_constr cs) in
-	  let cst = 
+	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
 	    if cb.const_polymorphic then cst
-	    else (*FIXME MS: computed above *)
-	      (Univ.UContext.constraints (Future.force cb.const_universes)) +++ cst 
+	    else ccst +++ cst 
 	  in
             c, cst
       in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 673b12b2c..73d5c5db2 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -17,7 +17,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 type cooking_info = { 
   modlist : work_list; 
   abstract : Context.named_context in_universe_context } 
-type proofterm = (constr * Univ.constraints) Future.computation
+type proofterm = (constr * Univ.universe_context) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of cooking_info list * proofterm
@@ -99,7 +99,7 @@ let force_constraints = function
   | NoIndirect(_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       match !get_univ dp i with
-      | None -> Univ.Constraint.empty
+      | None -> Univ.UContext.empty
       | Some u -> Future.force u
 
 let get_constraints = function
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 71f491754..fee15e405 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -19,7 +19,7 @@ open Mod_subst
     When it is [turn_indirect] the data is relocated to an opaque table
     and the [opaque] is turned into an index. *)
 
-type proofterm = (constr * Univ.constraints) Future.computation
+type proofterm = (constr * Univ.universe_context) Future.computation
 type opaque
 
 (** From a [proofterm] to some [opaque]. *)
@@ -31,9 +31,9 @@ val turn_indirect : opaque -> opaque
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor configured below. *)
 val force_proof : opaque -> constr
-val force_constraints : opaque -> Univ.constraints
+val force_constraints : opaque -> Univ.universe_context
 val get_proof : opaque -> Term.constr Future.computation
-val get_constraints : opaque -> Univ.constraints Future.computation option
+val get_constraints : opaque -> Univ.universe_context Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
 val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
@@ -66,7 +66,7 @@ val set_indirect_creator :
 val set_indirect_opaque_accessor :
   (DirPath.t -> int -> Term.constr Future.computation) -> unit
 val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.constraints Future.computation option) -> unit
+  (DirPath.t -> int -> Univ.universe_context Future.computation option) -> unit
 val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit
 val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit
 val reset_indirect_creator : unit -> unit
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 35577239b..deabf1bcf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -298,11 +298,11 @@ 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 c = match c with
-    | Def c -> Mod_subst.force_constr c
-    | OpaqueDef o -> Opaqueproof.force_proof o
+  let c, univs = match c with
+    | Def c -> Mod_subst.force_constr c, univs
+    | OpaqueDef o -> Opaqueproof.force_proof o, Opaqueproof.force_constraints o
     | _ -> assert false in
-  let senv' = push_context (Future.join de.Entries.const_entry_universes) senv in
+  let senv' = push_context univs senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
@@ -332,9 +332,15 @@ let globalize_constant_universes cb =
   if cb.const_polymorphic then
     Now Univ.Constraint.empty
   else
-    (match Future.peek_val cb.const_universes with
-    | Some c -> Now (Univ.UContext.constraints c)
-    | None -> Later (Future.chain ~pure:true cb.const_universes Univ.UContext.constraints))
+    match cb.const_body with
+    | (Undef _ | Def _) -> Now (Univ.UContext.constraints cb.const_universes)
+    | OpaqueDef lc ->
+      match Opaqueproof.get_constraints lc with
+      | None -> Now (Univ.UContext.constraints cb.const_universes)
+      | Some fc ->
+        match Future.peek_val fc with
+        | None -> Later (Future.chain ~pure:true fc Univ.UContext.constraints)
+        | Some c -> Now (Univ.UContext.constraints c)
       
 let globalize_mind_universes mb =
   if mb.mind_polymorphic then
@@ -751,7 +757,7 @@ let import lib cst vodigest senv =
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
   let env = Environ.add_constraints mb.mod_constraints senv.env in
-  let env = Environ.add_constraints cst env in
+  let env = Environ.push_context cst env in
   (mp, lib.comp_natsymbs),
   { senv with
     env =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ad2148ead..5b5457c38 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -140,7 +140,7 @@ val export :
     module_path * compiled_library * native_library
 
 (* Constraints are non empty iff the file is a vi2vo *)
-val import : compiled_library -> Univ.constraints -> vodigest ->
+val import : compiled_library -> Univ.universe_context -> vodigest ->
   (module_path * Nativecode.symbol array) safe_transformer
 
 (** {6 Safe typing judgments } *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 56e94ba0d..61420d7ca 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -308,7 +308,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let u1 = inductive_instance mind1 in
       let arity1,cst1 = constrained_type_of_inductive env 
 	((mind1,mind1.mind_packets.(i)),u1) in
-      let cst2 = UContext.constraints (Future.force cb2.const_universes) in
+      let cst2 = Declareops.constraints_of_constant cb2 in 
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, arity1, typ2) in
@@ -323,7 +323,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
       let u1 = inductive_instance mind1 in
       let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
-      let cst2 = UContext.constraints (Future.force cb2.const_universes) in
+      let cst2 = Declareops.constraints_of_constant cb2 in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, ty1, ty2) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 27ab90aa5..780c14a20 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -89,7 +89,7 @@ let handle_side_effects env body side_eff =
               let t = sub c 1 (Vars.lift 1 t) in
 		mkLetIn (cname c, b, b_ty, t)
 	    else 
-	      let univs = Future.force cb.const_universes in
+	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
       | OpaqueDef b -> 
           let b = Opaqueproof.force_proof b in
@@ -99,7 +99,7 @@ let handle_side_effects env body side_eff =
               let t = sub c 1 (Vars.lift 1 t) in
 		mkApp (mkLambda (cname c, b_ty, t), [|b|]) 
 	    else
-	      let univs = Future.force cb.const_universes in
+	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
     in
       List.fold_right fix_body cbl t
@@ -120,10 +120,10 @@ let infer_declaration env kn dcl =
       let env = push_context uctx env in
       let j = infer env t in
       let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, RegularArity t, None, poly, Future.from_val uctx, false, ctx
+      Undef nl, RegularArity t, None, poly, uctx, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true } as c) ->
-      let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *)
+      let env = push_context c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -133,12 +133,13 @@ let infer_declaration env kn dcl =
           let j = hcons_j j in
           let _typ = constrain_type env j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, Univ.empty_constraint) in
+          j.uj_val, Univ.UContext.empty) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes,
+      def, RegularArity typ, None, c.const_entry_polymorphic, 
+	c.const_entry_universes,
 	c.const_entry_inline_code, c.const_entry_secctx
   | DefinitionEntry c ->
-      let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *)
+      let env = push_context c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let body, side_eff = Future.join body in
@@ -211,7 +212,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         | OpaqueDef lc ->
             let vars = global_vars_set env (Opaqueproof.force_proof lc) in
             (* we force so that cst are added to the env immediately after *)
-            ignore(Future.join univs);
+            ignore(Opaqueproof.force_constraints lc);
             !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;
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
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 49f833590..3f728ddcd 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -183,7 +183,6 @@ let is_rec names =
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
     | GProj (loc, p, c) -> lookup names c
     | GCast(_,b,_) -> lookup names b
-    | GProj _ -> error "GProj not handled"
     | GRec _ -> error "GRec not handled"
     | GIf(_,b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 897c8765b..b68d9762e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1117,7 +1117,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     let schemes =
       Array.of_list scheme
     in
-    let proving_tac =
+    let _proving_tac =
       prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos
     in
     Array.iteri
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index fdcce914d..ada497ece 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -99,7 +99,7 @@ let typeclass_univ_instance (cl,u') =
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-	  if cb.const_polymorphic then Univ.UContext.instance (Future.force cb.const_universes)
+	  if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
 	  else Univ.Instance.empty
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 87d7e0980..e36019887 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -378,17 +378,18 @@ let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = Declareops.body_of_constant cb in
   let typ = ungeneralized_type_of_constant_type cb.const_type in
+  let univs = Declareops.universes_of_constant cb in
   hov 0 (pr_polymorphic cb.const_polymorphic ++
     match val_0 with
     | None ->
 	str"*** [ " ++
 	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_universe_ctx (Future.force cb.const_universes)
+	Printer.pr_universe_ctx univs
     | _ ->
 	print_basename sp ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
-        Printer.pr_universe_ctx (Future.force cb.const_universes))
+        Printer.pr_universe_ctx univs)
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 1b329dbc4..22262036e 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -36,8 +36,8 @@ let start_proof (id : Id.t) str hyps c ?init_tac terminator =
 
 let cook_this_proof p =
   match p with
-  | { Proof_global.id;entries=[constr];persistence;constraints } ->
-      (id,(constr,constraints,persistence))
+  | { Proof_global.id;entries=[constr];persistence;universes } ->
+      (id,(constr,universes,persistence))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let cook_proof () =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index b99bbe872..3efc644e0 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -69,11 +69,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Entries.definition_entry * Univ.constraints * goal_kind))
+    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Entries.definition_entry * Univ.constraints * goal_kind))
+    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 29810eb9a..9be159640 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -63,12 +63,14 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
+type proof_universes = Universes.universe_opt_subst Univ.in_universe_context
 
 type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  constraints : Univ.constraints;
+  universes: proof_universes;
+  (* constraints : Univ.constraints; *)
 }
 
 type proof_ending =
@@ -79,10 +81,6 @@ type proof_ending =
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
-type 'a proof_decl_hook =
-  Universes.universe_opt_subst Univ.in_universe_context -> 
-  Decl_kinds.locality -> Globnames.global_reference -> 'a
-
 type pstate = {
   pid : Id.t;
   terminator : proof_terminator Ephemeron.key;
@@ -266,65 +264,52 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
+let nf_body nf b =
+  let aux (c, t) = (nf c, t) in
+    Future.chain ~pure:true b aux
+
 let close_proof ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let fpl, univs = Future.split2 fpl in
-  let () = if poly || now then ignore (Future.compute univs) in
-  let entries = Future.map2 (fun p (c, (t, octx)) ->
-    let compute_univs (usubst, uctx) = 
-      let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in
-      let compute_c_t (c, eff) =
-	let c, t = 
-	  if not now then nf c, nf t
-	  else (* Already normalized below *) c, nf t 
-	in
-	let univs =
-	  Univ.LSet.union (Universes.universes_of_constr c)
-	    (Universes.universes_of_constr t)
-	in
-	let ctx, subst = 
-	  Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) univs 
-	in
-	let nf x = Vars.subst_univs_level_constr subst x in
-	  (nf c, eff), nf t, Univ.ContextSet.to_context ctx
-      in
-        Future.chain ~pure:true p compute_c_t
-    in
-    let ans = Future.chain ~pure:true univs compute_univs in
-    let ans = Future.join ans in
-    let p = Future.chain ~pure:true ans (fun (x, _, _) -> x) in
-    let t = Future.chain ~pure:true ans (fun (_, x, _) -> x) in
-    let univs = Future.chain ~pure:true ans (fun (_, _, x) -> x) in
-    let t = Future.force t in
-      { Entries.
-	const_entry_body = p;
-	const_entry_secctx = section_vars;
-	const_entry_type  = Some t;
-	const_entry_inline_code = false;
-	const_entry_opaque = true;
-	const_entry_universes = univs;
-        const_entry_feedback = None;
-	const_entry_polymorphic = pi2 strength;
-	const_entry_proj = None}) fpl initial_goals in
-  let globaluctx = 
-    if not poly then
-      List.fold_left (fun acc (c, (t, octx)) -> 
-	Univ.ContextSet.union octx acc)
-	Univ.ContextSet.empty initial_goals
-    else Univ.ContextSet.empty
-  in
-  let _ = 
+  let (subst, univs as univsubst), nf = 
     if poly || now then
-      List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries
+      let usubst, uctx = Future.force univs in
+      let ctx, subst = 
+	Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) 
+      in
+      let nf x = 
+	let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in
+	  Vars.subst_univs_level_constr subst (nf x)
+      in
+      let subst = 
+	Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst)
+      in
+	(subst, Univ.ContextSet.to_context ctx), nf
+    else
+      let ctx = 
+	List.fold_left (fun acc (c, (t, octx)) -> 
+	  Univ.ContextSet.union octx acc)
+	  Univ.ContextSet.empty initial_goals
+      in
+	(Univ.LMap.empty, Univ.ContextSet.to_context ctx), (fun x -> x)
   in
-(*  let hook = Option.map (fun f -> 
-    if poly || now then f (Future.join univs) 
-    else f (Univ.LMap.empty,Univ.UContext.empty))
-    hook
-  in*) (* FIXME *)
-  { id = pid; entries = entries; persistence = strength; constraints = Univ.ContextSet.constraints globaluctx },
+  let entries =
+    Future.map2 (fun p (c, (t, octx)) -> { Entries.
+      const_entry_body = nf_body nf p;
+      const_entry_secctx = section_vars;
+      const_entry_feedback = feedback_id;
+      const_entry_type  = Some (nf t);
+      const_entry_inline_code = false;
+      const_entry_opaque = true;
+      const_entry_universes = univs;
+      const_entry_polymorphic = poly;
+      const_entry_proj = None})
+    fpl initial_goals in
+  if now then
+    List.iter (fun x ->ignore(Future.force x.Entries.const_entry_body)) entries;
+  { id = pid; entries = entries; persistence = strength; universes = univsubst },
   Ephemeron.get terminator
 
 type closed_proof_output = Entries.proof_output list * 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6c11ee9b4..1ad1cebf8 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,10 +46,6 @@ exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
 (** @raise NoCurrentProof when outside proof mode. *)
 
-type 'a proof_decl_hook =
-  Universes.universe_opt_subst Univ.in_universe_context -> 
-  Decl_kinds.locality -> Globnames.global_reference -> 'a
-
 (** When a proof is closed, it is reified into a [proof_object], where
     [id] is the name of the proof, [entries] the list of the proof terms
     (in a form suitable for definitions). Together with the [terminator]
@@ -57,11 +53,13 @@ type 'a proof_decl_hook =
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
+type proof_universes = Universes.universe_opt_subst Univ.in_universe_context
 type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  constraints : Univ.constraints;
+  universes: proof_universes;
+  (* constraints : Univ.constraints; *)
   (** guards : lemma_possible_guards; *)
 }
 
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index f6ba5341e..ebbb04087 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -1,216 +1 @@
-module NonLogical =
-struct
-type 'a t = unit -> 'a
-
-type 'a ref = 'a Pervasives.ref
-
-let ret = fun a -> (); fun () -> a
-
-let bind = fun a k -> (); fun () -> k (a ()) ()
-
-let ignore = fun a -> (); fun () -> ignore (a ())
-
-let seq = fun a k -> (); fun () -> a (); k ()
-
-let new_ref = fun a -> (); fun () -> Pervasives.ref a
-
-let set = fun r a -> (); fun () -> Pervasives.(:=) r a
-
-let get = fun r -> (); fun () -> Pervasives.(!) r
-
-let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
-
-let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()
-
-let read_line = fun () -> try Pervasives.read_line () with e -> raise e ()
-
-let print_char = fun c -> (); fun () -> print_char c
-
-let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
-
-let timeout = fun n t -> (); fun () ->
-  let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
-  let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-  Pervasives.ignore (Unix.alarm n);
-  let restore_timeout () =
-    Pervasives.ignore (Unix.alarm 0);
-    Sys.set_signal Sys.sigalrm psh
-  in
-  try
-    let res = t () in
-    restore_timeout ();
-    res
-  with
-  | e -> restore_timeout (); Pervasives.raise e
-
-let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
-
-end
-
-
-type ('a, 'b) list_view =
-| Nil of exn
-| Cons of 'a * 'b
-
-type proofview = { initial : (Term.constr*Term.types) list; solution : Evd.evar_map; comb : Goal.goal list }
-
-type logicalState = proofview
-
-type logicalMessageType = bool * (Goal.goal list * Goal.goal list)
-
-type logicalEnvironment = Environ.env
-
-type message = logicalMessageType
-type environment = logicalEnvironment
-type state = logicalState
-
-module Logical =
-struct
-
-type 'a ioT = 'a NonLogical.t
-
-type 'a logicT = { logic : 'r. ('a -> (exn -> 'r ioT) -> 'r ioT) -> (exn -> 'r ioT) -> 'r ioT }
-
-type 'a writerT = { writer : 'r. ('a -> message -> 'r logicT) -> 'r logicT }
-
-type 'a readerT = { reader : 'r. ('a -> 'r writerT) -> environment -> 'r writerT }
-
-type 'a stateT = { state : 'r. ('a -> state -> 'r readerT) -> state -> 'r readerT }
-
-type 'a t = 'a stateT
-
-let empty_message = (true, ([], []))
-
-let ret x = { state = fun k s -> k x s }
-
-let bind m f = { state = fun k s -> m.state (fun x s -> (f x).state k s) s }
-
-let ignore m = { state = fun k s -> m.state (fun _ s -> k () s) s }
-
-let seq m n =
-  { state = fun k s -> m.state (fun () s -> n.state k s) s }
-
-let set s =
-  { state = fun k _ -> k () s }
-
-let get = { state = fun k s -> k s s }
-
-let current = { state = fun k s -> { reader = fun kr e -> (k e s).reader kr e } }
-
-let join (b1, (l1, r1)) (b2, (l2, r2)) =
-  (b1 && b2, (List.append l1 l2, List.append r1 r2))
-
-let put msg =
-  { state = fun k s ->
-    let m = k () s in
-    { reader = fun kr e ->
-      let m = m.reader kr e in
-      { writer = fun kw -> m.writer
-        (fun x nmsg -> kw x (join msg nmsg))
-      }
-    }
-  }
-
-let zero err =
-  { state = fun k s ->
-    { reader = fun kr e ->
-      { writer = fun kw ->
-        { logic = fun sk fk -> fk err }
-      }
-    }
-  }
-
-let plus m f =
-  { state = fun k s ->
-    let m = m.state k s in
-    { reader = fun kr e ->
-      let m = m.reader kr e in
-      { writer = fun kw ->
-        let m = m.writer kw in
-        { logic = fun sk fk ->
-          let plus_fk err = ((((f err).state k s).reader kr e).writer kw).logic sk fk in
-          m.logic sk plus_fk
-        }
-      }
-    }
-  }
-
-let srun_state x s = { reader = fun kr _ -> kr (x, s) }
-let srun_reader x = { writer = fun kw -> kw x empty_message }
-let srun_writer x msg = { logic = fun sk fk -> sk (x, msg) fk }
-
-let srun_logic_sk x fk =
-  let next err =
-    let ans = fk err in { logic = fun sk fk ->
-    NonLogical.bind ans (function
-    | Nil err -> fk err
-    | Cons (y, n) -> sk x (fun err -> (n err).logic sk fk))
-  } in
-  let ans = Cons (x, next) in
-  NonLogical.ret ans
-
-let srun_logic_fk err = NonLogical.ret (Nil err)
-
-let split_next k s kr e kw sk fk = (); function
-| Nil _ as x ->
-  let m = k x s in
-  let m = m.reader kr e in
-  let m = m.writer kw in
-  m.logic sk fk
-| Cons (((x, s), msg), next) ->
-  let next err =
-    let next = next err in {
-    state = fun k s -> {
-      reader = fun kr e -> {
-        writer = fun kw -> {
-          logic = fun sk fk ->
-            let sk ((x, s), msg) fk =
-              let kw x nmsg = kw x (join msg nmsg) in
-              (((k x s).reader kr e).writer kw).logic sk fk
-            in
-            next.logic sk fk
-        }
-      }
-    }
-  } in
-  let m = k (Cons (x, next)) s in
-  let m = m.reader kr e in
-  let m = m.writer (fun x nmsg -> kw x (join msg nmsg)) in
-  m.logic sk fk
-
-let split m =
-  { state = fun k s ->
-    let m = m.state srun_state s in
-    { reader = fun kr e ->
-      let m = m.reader srun_reader e in
-      { writer = fun kw ->
-        let m = m.writer srun_writer in
-        { logic = fun sk fk ->
-          let m = m.logic srun_logic_sk srun_logic_fk in
-          NonLogical.bind m (split_next k s kr e kw sk fk)
-        }
-      }
-    }
-  }
-
-let lift m =
-  { state = fun k s ->
-    { reader = fun kr e ->
-      { writer = fun kw ->
-        { logic = fun sk fk ->
-          let lift x = (((k x s).reader kr e).writer kw).logic sk fk in
-          NonLogical.bind m lift
-        }
-      }
-    }
-  }
-
-let run m e s =
-  let m = m.state srun_state s in
-  let m = m.reader srun_reader e in
-  let m = m.writer srun_writer in
-  let run_fk err = NonLogical.raise (Proof_errors.TacticFailure err) in
-  let run_sk x _ = NonLogical.ret x in
-  m.logic run_sk run_fk
-
-end
+include Proofview_gen
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 4f9bc8c44..e9831f834 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -171,7 +171,7 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
   let const = adjust_guardness_conditions const do_guard in
   let k = Kindops.logical_kind_of_goal_kind kind in
   (* Add global constraints necessary to check the type of the proof *)
-  let () = Global.add_constraints cstrs in
+  let () = Global.push_context (snd cstrs) in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
 	let c = SectionLocalDef const in
diff --git a/stm/stm.ml b/stm/stm.ml
index 69e73089e..8c034c030 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -744,7 +744,7 @@ end = struct
             | Declarations.SEsubproof(_,
                { Declarations.const_body = Declarations.OpaqueDef f;
 		 const_universes = univs } ) ->
-                Opaqueproof.join_opaque f; ignore (Future.join univs) (* FIXME: MS: needed?*)
+                Opaqueproof.join_opaque f
             | _ -> ())
           se) (fst l);
           l, Unix.gettimeofday () -. wall_clock in
@@ -808,7 +808,7 @@ end = struct
         | Declarations.OpaqueDef lc ->
             let uc = Option.get (Opaqueproof.get_constraints lc) in
             let uc =
-              Future.chain ~greedy:true ~pure:true uc Univ.hcons_constraints in
+              Future.chain ~greedy:true ~pure:true uc Univ.hcons_universe_context in
             let pr = Opaqueproof.get_proof lc in
             let pr = Future.chain ~greedy:true ~pure:true pr discharge in
             let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
@@ -816,7 +816,7 @@ end = struct
             let extra = Future.join uc in
             u.(bucket) <- uc;
             p.(bucket) <- pr;
-            u, Univ.union_constraint cst extra, false
+            u, Univ.UContext.union cst extra, false
         | _ -> assert false
   
   let check_task name l i =
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 2c971ec24..bd6e2ca8f 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -119,7 +119,7 @@ Lemma eq_sigT_eq_dep :
     existT P p x = existT P q y -> eq_dep p x q y.
 Proof.
   intros.
-  dependent rewrite H. 
+  dependent rewrite H.
   apply eq_dep_intro.
 Qed.
 
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index b406e5302..2a408e03d 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -128,7 +128,7 @@ let define internal id c p univs =
     const_entry_type = None;
     const_entry_proj = None;
     const_entry_polymorphic = p;
-    const_entry_universes = Future.from_val (Evd.evar_context_universe_context ctx);
+    const_entry_universes = Evd.evar_context_universe_context ctx;
     const_entry_opaque = false;
     const_entry_inline_code = false;
     const_entry_feedback = None;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 757cdbea9..57b428b5c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -122,7 +122,7 @@ let define id internal ctx c t =
         const_entry_type = t;
 	const_entry_proj = None;
 	const_entry_polymorphic = true;
-	const_entry_universes = Future.from_val (Evd.universe_context ctx); (* FIXME *)
+	const_entry_universes = Evd.universe_context ctx;
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3b33a9184..97c95bfd8 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -786,8 +786,8 @@ let rec string_of_list sep f = function
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
 
-let solve_by_tac evi t poly subst ctx =
-  let id = Id.of_string "H" in
+let solve_by_tac name evi t poly subst ctx =
+  let id = name in
   let concl = Universes.subst_opt_univs_constr subst evi.evar_concl in
   (* spiwack: the status is dropped *)
   let (entry,_,subst) = Pfedit.build_constant_by_tactic 
@@ -905,7 +905,7 @@ and solve_obligation_by_tac prg obls i tac =
 		  | None -> snd (get_default_tactic ())
 	    in
 	    let t, subst, ctx = 
-	      solve_by_tac (evar_of_obligation obl) tac 
+	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac 
 	        (pi2 prg.prg_kind) prg.prg_subst prg.prg_ctx
 	    in
 	      obls.(i) <- declare_obligation {prg with prg_subst = subst} obl t ctx;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 56493bae8..af7f364f3 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
                     const_entry_secctx = None;
                     const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
-		    const_entry_universes = Future.from_val ctx;
+		    const_entry_universes = ctx;
 		    const_entry_proj = projinfo;
                     const_entry_opaque = false;
                     const_entry_inline_code = false;
-- 
cgit v1.2.3