- Fix bug preventing apply from unfolding Fixpoints.

- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.

Conflicts:
	kernel/univ.ml
	tactics/tactics.ml
	theories/Logic/EqdepFacts.v

2 files changed, 6 insertions, 6 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index e9831f8347..9cbd89e8b8 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -49,7 +49,7 @@ let adjust_guardness_conditions const = function
      let env = Global.env() in
      { const with const_entry_body =
         Future.chain ~greedy:true ~pure:true const.const_entry_body
-        (fun (body, eff) ->
+        (fun ((body, ctx), eff) ->
           match kind_of_term body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
 (*      let possible_indexes =
@@ -60,8 +60,8 @@ let adjust_guardness_conditions const = function
               let indexes =
 	        search_guard Loc.ghost env
                   possible_indexes fixdecls in
-              mkFix ((indexes,0),fixdecls),  eff
-          | _ -> body, eff) }
+		(mkFix ((indexes,0),fixdecls), ctx), eff
+          | _ -> (body, ctx), eff) }
 
 let find_mutually_recursive_statements thms =
     let n = List.length thms in
@@ -409,7 +409,7 @@ let start_proof_com kind thms hook =
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
-  let ctxset = Evd.get_universe_context_set evd in
+  let ctxset = Evd.universe_context_set evd in
   let thms = List.map (fun (n, (t, info)) -> (n, ((nf t, ctxset), info)))
     thms
   in
diff --git a/stm/stm.ml b/stm/stm.ml
index 8c034c030e..0136e52105 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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_universe_context in
+              Future.chain ~greedy:true ~pure:true uc Univ.hcons_universe_context_set 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.UContext.union cst extra, false
+            u, Univ.ContextSet.union cst extra, false
         | _ -> assert false
   
   let check_task name l i =