- 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

1 files changed, 11 insertions, 5 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0f296c6af..ab2a16575 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -922,7 +922,7 @@ let prepare_hint check env init (sigma,c) =
   let c' = iter c in
     if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Evd.diff sigma init in
-      IsConstr (c', Evd.get_universe_context_set diff)
+      IsConstr (c', Evd.universe_context_set diff)
 
 let interp_hints poly =
   fun h ->
@@ -1164,12 +1164,18 @@ let unify_resolve_gen poly = function
   | Some flags -> unify_resolve poly flags
 
 let exact poly (c,clenv) =
-  let c' = 
+  let ctx, c' = 
     if poly then
       let evd', subst = Evd.refresh_undefined_universes clenv.evd in
-	subst_univs_level_constr subst c 
-    else c
-  in exact_check c'
+      let ctx = Evd.evar_universe_context evd' in
+	ctx, subst_univs_level_constr subst c 
+    else 
+      let ctx = Evd.evar_universe_context clenv.evd in
+	ctx, c
+  in 
+    fun gl ->
+      tclTHEN (Refiner.tclEVARS (Evd.merge_universe_context (project gl) ctx)) 
+	(exact_check c') gl
     
 (* Util *)