- 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, 15 insertions, 8 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 780c14a208..0959fa7033 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -57,6 +57,8 @@ let local_constrain_type env j = function
 
 (* Insertion of constants and parameters in environment. *)
 
+let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
+
 let handle_side_effects env body side_eff =
   let handle_sideff t se =
     let cbl = match se with
@@ -127,13 +129,14 @@ let infer_declaration env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
+        Future.chain ~greedy:true ~pure:true body (fun ((body, ctx), side_eff) ->
           let body = handle_side_effects env body side_eff in
-          let j = infer env body in
+	  let env' = push_context_set ctx env in
+          let j = infer env' body in
           let j = hcons_j j in
-          let _typ = constrain_type env j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
+          let _typ = constrain_type env' j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, Univ.UContext.empty) in
+          j.uj_val, ctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None, c.const_entry_polymorphic, 
 	c.const_entry_universes,
@@ -142,7 +145,8 @@ let infer_declaration env kn dcl =
       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
+      let (body, ctx), side_eff = Future.join body in
+      let env = push_context_set ctx env in
       let body = handle_side_effects env body side_eff in
       let def, typ, proj = 
 	match c.const_entry_proj with
@@ -168,9 +172,12 @@ let infer_declaration env kn dcl =
 	  let def = Def (Mod_subst.from_val j.uj_val) in
 	    def, typ, None
       in
+      let univs = Univ.UContext.union c.const_entry_universes 
+	(Univ.ContextSet.to_context ctx)
+      in
 	feedback_completion_typecheck feedback_id;
 	def, typ, proj, c.const_entry_polymorphic,
-        c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx
+        univs, c.const_entry_inline_code, c.const_entry_secctx
 
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
@@ -281,6 +288,6 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let handle_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
-    ce.const_entry_body (fun (body, side_eff) ->
-       handle_side_effects env body side_eff, Declareops.no_seff);
+    ce.const_entry_body (fun ((body, ctx), side_eff) ->
+      (handle_side_effects env body side_eff, ctx), Declareops.no_seff);
 }