From 1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 8 Nov 2013 11:31:22 +0100
Subject: - 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
---
 stm/lemmas.ml | 8 ++++----
 stm/stm.ml    | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'stm')

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 =
-- 
cgit v1.2.3