Rework handling of universes on top of the STM, allowing for delayed

computation in case of non-polymorphic proofs. Also fix plugins after
forgotten merge conflicts. Still does not compile everything.

22 files changed, 126 insertions, 155 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 24e029bc0..1bc3bbd15 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -62,8 +62,8 @@ type definition_entry = {
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
   const_entry_polymorphic : bool;
-  const_entry_universes : Univ.universe_context;
-  const_entry_proj   : projection option;
+  const_entry_universes   : Univ.universe_context Future.computation;
+  const_entry_proj        : projection option;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 093797fc0..7d49e452c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -301,7 +301,7 @@ let push_named_def (id,de) senv =
     | Def c -> Mod_subst.force_constr c
     | OpaqueDef o -> Opaqueproof.force_proof o
     | _ -> assert false in
-  let senv' = push_context de.Entries.const_entry_universes senv in
+  let senv' = push_context (Future.join de.Entries.const_entry_universes) senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9aa688fc7..352ef40d9 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -101,7 +101,7 @@ let infer_declaration env kn dcl =
       Undef nl, t, None, poly, Future.from_val uctx, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true } as c) ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *)
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -113,10 +113,10 @@ let infer_declaration env kn dcl =
           feedback_completion_typecheck feedback_id;
           j.uj_val, Univ.empty_constraint) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      def, typ, None, c.const_entry_polymorphic, Future.from_val c.const_entry_universes,
+      def, 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 c.const_entry_universes env in
+      let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *)
       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
@@ -127,7 +127,7 @@ let infer_declaration env kn dcl =
       feedback_completion_typecheck feedback_id;
       let def = Def (Mod_subst.from_val j.uj_val) in
       def, typ, None, c.const_entry_polymorphic,
-        Future.from_val c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx
+        c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx
 
 (* let global_vars_set_constant_type env = function *)
 (*   | NonPolymorphicType t -> global_vars_set env t *)
diff --git a/library/declare.ml b/library/declare.ml
index 452504bf0..41f50753f 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 de.const_entry_universes) in
+	(Univ.ContextSet.of_context (Future.force 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 [];
@@ -194,17 +194,17 @@ let declare_constant_common id cst =
   Notation.declare_ref_arguments_scope (ConstRef c);
   c
 
-let definition_entry ?(opaque=false) ?types 
-    ?(poly=false) ?(univs=Univ.UContext.empty) body =
-  { const_entry_body = Future.from_val (body,Declareops.no_seff);
+let definition_entry ?(opaque=false) ?(inline=false) ?types 
+    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
+  { const_entry_body = Future.from_val (body,eff);
     const_entry_secctx = None;
     const_entry_type = types;
     const_entry_proj = None;
     const_entry_polymorphic = poly;
-    const_entry_universes = univs;
+    const_entry_universes = Future.from_val univs;
     const_entry_opaque = opaque;
     const_entry_feedback = None;
-    const_entry_inline_code = false}
+    const_entry_inline_code = inline}
 
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
@@ -234,7 +234,7 @@ let declare_sideff se =
         const_entry_inline_code = false;
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
-	const_entry_universes = Future.join cb.const_universes;
+	const_entry_universes = cb.const_universes;
 	const_entry_proj = None;
     });
     cst_hyps = [] ;
diff --git a/library/declare.mli b/library/declare.mli
index 848bab618..ed3e4dcc3 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -48,8 +48,8 @@ type internal_flag =
   | UserVerbose
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
-val definition_entry : ?opaque:bool -> ?types:types -> 
-  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
+  ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects ->
   constr -> definition_entry
 
 val declare_constant :
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2adc82505..88693c196 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -340,19 +340,7 @@ let generate_functional_principle
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce =
-          { const_entry_body =
-              Future.from_val (value,Declareops.no_seff);
-            const_entry_secctx = None;
-	    const_entry_type = None;	
-	    const_entry_polymorphic = false;
-	    const_entry_universes = Univ.UContext.empty (*FIXME*);
-	    const_entry_proj = None;
-	    const_entry_opaque = false;
-            const_entry_feedback = None;
-	    const_entry_inline_code = false
-	  }
-	in
+	let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *)
 	ignore(
 	  Declare.declare_constant
 	    name
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 7ed8e03a9..ae05fbdc3 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -152,18 +152,10 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c
 let decl_constant na ctx c =
   let vars = Universes.universes_of_constr c in
   let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
-  mkConst(declare_constant (Id.of_string na) (DefinitionEntry
-    { const_entry_body = Future.from_val (c, Declareops.no_seff);
-      const_entry_secctx = None;
-      const_entry_type = None;
-      const_entry_polymorphic = false;
-      const_entry_universes = Univ.ContextSet.to_context ctx;
-      const_entry_proj = None;
-      const_entry_opaque = true;
-      const_entry_inline_code = false;
-      const_entry_feedback = None;
-    },
-    IsProof Lemma))
+  mkConst(declare_constant (Id.of_string na) 
+	    (DefinitionEntry (definition_entry ~opaque:true
+				~univs:(Univ.ContextSet.to_context ctx) c),
+	     IsProof Lemma))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
@@ -442,11 +434,11 @@ let theory_to_obj : ring_info -> obj =
 
 let setoid_of_relation env evd a r =
   try
-    let evm = !evd, Int.Set.empty in
-    let evm, refl = Rewrite.PropGlobal.get_reflexive_proof env evm a r in
-    let evm, sym = Rewrite.PropGlobal.get_symmetric_proof env evm a r in
-    let evm, trans = Rewrite.PropGlobal.get_transitive_proof env evm a r in
-      evd := fst evm;
+    let evm = !evd in
+    let evm, refl = Rewrite.get_reflexive_proof env evm a r in
+    let evm, sym = Rewrite.get_symmetric_proof env evm a r in
+    let evm, trans = Rewrite.get_transitive_proof env evm a r in
+      evd := evm;
       lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
   with Not_found ->
     error "cannot find setoid relation"
@@ -682,9 +674,9 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
   let lemma2 = params.(4) in
 
   let lemma1 =
-    decl_constant (Id.to_string name^"_ring_lemma1") ctx (Future.from_val ( lemma1,Declareops.no_seff)) in
+    decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in
   let lemma2 =
-    decl_constant (Id.to_string name^"_ring_lemma2") ctx (Future.from_val ( lemma2,Declareops.no_seff)) in
+    decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -724,10 +716,16 @@ type 'constr ring_mod =
   | Div_spec of Constrexpr.constr_expr
 
 
+let ic_coeff_spec = function
+  | Computational t -> Computational (ic_unsafe t)
+  | Morphism t -> Morphism (ic_unsafe t)
+  | Abstract -> Abstract
+
+
 VERNAC ARGUMENT EXTEND ring_mod
-  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic_unsafe eq_test)) ]
+  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
   | [ "abstract" ] -> [ Ring_kind Abstract ]
-  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic_unsafe morph)) ]
+  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
   | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
   | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
   | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
@@ -754,7 +752,7 @@ let process_ring_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_kind k -> set_once "ring kind" kind k
+      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k)
     | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
     | Pre_tac t -> set_once "preprocess tactic" pre t
     | Post_tac t -> set_once "postprocess tactic" post t
@@ -1026,18 +1024,18 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power
   let lemma4 = params.(6) in
   let cond_lemma =
     match inj with
-      | Some thm -> mkApp(constr_of params.(8),[|thm|])
-      | None -> constr_of params.(7) in
+      | Some thm -> mkApp(params.(8),[|thm|])
+      | None -> params.(7) in
   let lemma1 = decl_constant (Id.to_string name^"_field_lemma1")
-    ctx (Future.from_val (lemma1,Declareops.no_seff)) in
+    ctx lemma1 in
   let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") 
-    ctx (Future.from_val (lemma2,Declareops.no_seff)) in
+    ctx lemma2 in
   let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") 
-    ctx (Future.from_val (lemma3,Declareops.no_seff)) in
+    ctx lemma3 in
   let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") 
-    ctx (Future.from_val (lemma4,Declareops.no_seff)) in
+    ctx lemma4 in
   let cond_lemma = decl_constant (Id.to_string name^"_lemma5") 
-    ctx (Future.from_val (cond_lemma,Declareops.no_seff)) in
+    ctx cond_lemma in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -1083,7 +1081,7 @@ let process_field_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_mod(Ring_kind k) -> set_once "field kind" kind k
+      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k)
     | Ring_mod(Const_tac t) ->
         set_once "tactic recognizing constants" cst_tac t
     | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 5c060c3d6..67c9dd0a3 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -37,7 +37,7 @@ let interp_ascii dloc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,if Int.equal mp 0 then glob_false else glob_true,None)
+     GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None)
      :: (aux (n-1) (p/2)) in
   GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p)
 
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 5131a5f38..2b1410be6 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -182,8 +182,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([GRef (Loc.ghost, glob_ZERO, None, None);
-    GRef (Loc.ghost, glob_POS, None, None);
-    GRef (Loc.ghost, glob_NEG, None, None)],
+  ([GRef (Loc.ghost, glob_ZERO, None);
+    GRef (Loc.ghost, glob_POS, None);
+    GRef (Loc.ghost, glob_NEG, None)],
   uninterp_z,
   true)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7434979f8..f7548b6ca 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,7 +68,6 @@ type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  opt_subst : Universes.universe_opt_subst;
 }
 
 type proof_ending =
@@ -268,17 +267,29 @@ let get_open_goals () =
 
 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 evdref = ref (Proof.return proof) in
-  let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
-  let initial_goals = List.map (fun (c,t) -> (nf c, nf t)) initial_goals in
-  let ctx = Evd.universe_context !evdref 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) ->
-    let univs = 
-      Univ.LSet.union (Universes.universes_of_constr c)
-	(Universes.universes_of_constr t)
-    in 
-    let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) univs in
+    let compute_univs (usubst, uctx) = 
+      let nf = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst in
+      let compute_c_t (c, eff) =
+        let univs =
+          Univ.LSet.union (Universes.universes_of_constr c)
+            (Universes.universes_of_constr t)
+        in 
+        let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context uctx) univs 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;
@@ -286,14 +297,17 @@ let close_proof ?feedback_id ~now fpl =
     const_entry_feedback = feedback_id;
     const_entry_inline_code = false;
     const_entry_opaque = true;
-    const_entry_universes = Univ.ContextSet.to_context ctx;
+    const_entry_universes = univs;
     const_entry_polymorphic = pi2 strength;
     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; opt_subst = subst },
+  { id = pid; entries = entries; persistence = strength },
   Ephemeron.get terminator
 
+type closed_proof_output = Entries.proof_output list * 
+    Universes.universe_opt_subst Univ.in_universe_context
+
 let return_proof () =
   let { proof } = cur_pstate () in
   let initial_goals = Proof.initial_goals proof in
@@ -310,10 +324,14 @@ let return_proof () =
         error(str"Attempt to save a proof with existential " ++
               str"variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
+  let evd = Evd.nf_constraints evd in
+  let subst = Evd.universe_subst evd in
+  let ctx = Evd.universe_context evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-  List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals
+  let goals = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals in
+    goals, (subst, ctx)
 
 let close_future_proof ~feedback_id proof =
   close_proof ~feedback_id ~now:false proof
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e651bdfae..f10e991ea 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -61,7 +61,6 @@ type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  opt_subst : Universes.universe_opt_subst;
 }
 
 type proof_ending =
@@ -95,9 +94,13 @@ val close_proof : (exn -> exn) -> closed_proof
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
  * chained with a computation that completed the proof *)
-val return_proof : unit -> Entries.proof_output list
+
+type closed_proof_output = Entries.proof_output list * 
+    Universes.universe_opt_subst Univ.in_universe_context
+
+val return_proof : unit -> closed_proof_output
 val close_future_proof : feedback_id:Stateid.t ->
-  Entries.proof_output list Future.computation -> closed_proof
+  closed_proof_output Future.computation -> closed_proof
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 2aeb8141e..13194eb89 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -229,17 +229,8 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp
         | _ -> anomaly (Pp.str "Not a proof by induction") in
       match locality with
       | Discharge ->
-          let const = { const_entry_body =
-                Future.from_val (body_i,Declareops.no_seff);
-              const_entry_secctx = None;
-              const_entry_type = Some t_i;
-	      const_entry_proj = None;
-              const_entry_opaque = opaq;
-              const_entry_feedback = None;
-              const_entry_inline_code = false;
-	      const_entry_polymorphic = p;
-	      const_entry_universes = Univ.ContextSet.to_context ctx_i
-          } in
+          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
+	    ~univs:(Univ.ContextSet.to_context ctx_i) body_i in
 	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
           (Discharge,VarRef id,imps)
diff --git a/stm/stm.ml b/stm/stm.ml
index 0218c923b..3496a3e4f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -70,7 +70,7 @@ let vernac_parse eid s =
   ()
 
 module Vcs_ = Vcs.Make(Stateid)
-type future_proof = Entries.proof_output list Future.computation
+type future_proof = Proof_global.closed_proof_output Future.computation
 type proof_mode = string
 type depth = int
 type cancel_switch = bool ref
@@ -683,7 +683,7 @@ end = struct
   let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
 
   type response =
-    | RespBuiltProof of Entries.proof_output list * float
+    | RespBuiltProof of Proof_global.closed_proof_output * float
     | RespError of (* err, safe, msg, safe_states *)
         Stateid.t * Stateid.t * std_ppcmds *
           (Stateid.t * State.frozen_state) list
@@ -705,8 +705,9 @@ end = struct
  
   type task =
     | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
-        (Entries.proof_output list Future.assignement -> unit) * cancel_switch
+        (Proof_global.closed_proof_output Future.assignement -> unit) * cancel_switch
         * Loc.t * Future.UUID.t * string
+
   let pr_task = function
     | TaskBuildProof(_,bop,eop,_,_,_,_,s) ->
         "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
@@ -745,7 +746,7 @@ end = struct
 		 const_universes = univs } ) ->
                 Opaqueproof.join_opaque f; ignore (Future.join univs) (* FIXME: MS: needed?*)
             | _ -> ())
-          se) l;
+          se) (fst l);
           l, Unix.gettimeofday () -. wall_clock in
         VCS.print ();
         RespBuiltProof(rc,time)
@@ -895,7 +896,7 @@ end = struct
     let cancel_switch = ref false in
     if WorkersPool.is_empty () then
       if !Flags.compilation_mode = Flags.BuildVi then begin
-        let force () : Entries.proof_output list Future.assignement =
+        let force () : Proof_global.closed_proof_output Future.assignement =
           try `Val (build_proof_here_core loc stop ())
           with e -> let e = Errors.push e in `Exn e in
         let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 3bd83f46b..94268e020 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -66,7 +66,10 @@ let rec classify_vernac e =
     (* Nested vernac exprs *)
     | VernacProgram e -> classify_vernac e
     | VernacLocal (_,e) -> classify_vernac e
-    | VernacPolymorphic (b, e) -> classify_vernac e
+    | VernacPolymorphic (b, e) -> 
+      if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
+	fst (classify_vernac e), VtNow
+      else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
     | VernacTime e -> classify_vernac e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 23a7c9e53..81bc6a256 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -228,17 +228,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof = inversion_scheme env sigma t sort dep inv_op in
-  let entry = {
-    const_entry_body = Future.from_val (invProof,Declareops.no_seff);
-    const_entry_secctx = None;
-    const_entry_type = None;
-    const_entry_proj = None;
-    const_entry_polymorphic = true;
-    const_entry_universes = Univ.UContext.empty (*FIXME *);
-    const_entry_opaque = false;
-    const_entry_inline_code = false;
-    const_entry_feedback = None;
-  } in
+  let entry = definition_entry ~poly:true (*FIXME*) invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 83cb15f47..cbf33fdb4 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -2130,3 +2130,16 @@ let myapply id l gl =
   in
     tclTHEN (Refiner.tclEVARS !evars) (apply app) gl
 
+let get_lemma_proof f env evm x y = 
+  let (evm, _), c = f env (evm,Evar.Set.empty) x y in
+    evm, c
+
+let get_reflexive_proof =
+  get_lemma_proof PropGlobal.get_reflexive_proof
+
+let get_symmetric_proof = 
+  get_lemma_proof PropGlobal.get_symmetric_proof
+
+let get_transitive_proof = 
+  get_lemma_proof PropGlobal.get_transitive_proof
+  
diff --git a/toplevel/class.ml b/toplevel/class.ml
index d54efb632..eedb35acf 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -217,17 +217,9 @@ let build_id_coercion idf_opt source poly =
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      { const_entry_body = Future.from_val 
-          (mkCast (val_f, DEFAULTcast, typ_f),Declareops.no_seff);
-        const_entry_secctx = None;
-	const_entry_type = Some typ_f;
-	const_entry_proj = None;
-	const_entry_polymorphic = poly;
-	const_entry_universes = Univ.ContextSet.to_context ctx;
-        const_entry_opaque = false;
-        const_entry_inline_code = true;
-        const_entry_feedback = None;
-      } in
+      (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx)
+	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
+  in
   let decl = (constr_entry, IsDefinition IdentityCoercion) in
   let kn = declare_constant idf decl in
   ConstRef kn
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d2111f0fb..e8d2eda8a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -655,18 +655,8 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix (_,poly,_ as kind) ctx f def t imps =
-  let ce = {
-    const_entry_body = Future.from_val def;
-    const_entry_secctx = None;
-    const_entry_type = Some t;
-    const_entry_polymorphic = poly;
-    const_entry_universes = ctx;
-    const_entry_proj = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false;
-    const_entry_feedback = None;
-  } in
+let declare_fix (_,poly,_ as kind) ctx f (def,eff) t imps =
+  let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
   declare_definition f kind ce imps (fun _ r -> r)
 
 let _ = Obligations.declare_fix_ref := declare_fix
@@ -855,18 +845,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       let hook l gr = 
 	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
-	let ce =
-          { const_entry_body = Future.from_val (Evarutil.nf_evar !evdref body,Declareops.no_seff);
-            const_entry_secctx = None;
-	    const_entry_type = Some ty;
-	    (* FIXME *)
-	    const_entry_proj = None;
-	    const_entry_polymorphic = false;
-	    const_entry_universes = Evd.universe_context !evdref;
-            const_entry_feedback = None;
-        const_entry_opaque = false;
-        const_entry_inline_code = false}
-	in 
+	let univs = Evd.universe_context !evdref in
+	  (*FIXME poly? *)
+	let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 2a408e03d..b406e5302 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 = Evd.evar_context_universe_context ctx;
+    const_entry_universes = Future.from_val (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 c139f1910..757cdbea9 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 = Evd.universe_context ctx; (* FIXME *)
+	const_entry_universes = Future.from_val (Evd.universe_context ctx); (* FIXME *)
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d937c400a..158e45240 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -529,16 +529,9 @@ let subst_body expand prg =
 let declare_definition prg =
   let body, typ = subst_body true prg in
   let ce =
-    { const_entry_body = Future.from_val (body,Declareops.no_seff);
-      const_entry_secctx = None;
-      const_entry_type = Some typ;
-      const_entry_proj = None;
-      const_entry_polymorphic = pi2 prg.prg_kind;
-      const_entry_universes = Univ.ContextSet.to_context prg.prg_ctx;
-      const_entry_opaque = false;
-      const_entry_inline_code = false;
-      const_entry_feedback = None;
-    } in
+    definition_entry ~types:typ ~poly:(pi2 prg.prg_kind) 
+      ~univs:(Univ.ContextSet.to_context prg.prg_ctx) body
+  in
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 7411a6377..b144dfe43 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 = ctx;
+		    const_entry_universes = Future.from_val ctx;
 		    const_entry_proj = projinfo;
                     const_entry_opaque = false;
                     const_entry_inline_code = false;