- 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

9 files changed, 40 insertions, 42 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 1a1a4dfe7d..5129beeab3 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -645,7 +645,7 @@ let make_bl_scheme mind =
   let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (bl_goal, ctx)
     (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
   in
-  ([|ans|], Evd.empty_evar_universe_context), eff
+  ([|fst ans (*FIXME univs*)|], Evd.empty_evar_universe_context), eff
 
 let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
 
@@ -766,7 +766,7 @@ let make_lb_scheme mind =
   let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (lb_goal,Univ.ContextSet.empty)
     (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
-  ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), eff
+  ([|fst ans|], Evd.empty_evar_universe_context (* FIXME *)), eff
 
 let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
 
@@ -939,7 +939,7 @@ let make_eq_decidability mind =
     (compute_dec_goal (ind,u) lnamesparrec nparrec, Univ.ContextSet.empty)
     (compute_dec_tact ind lnamesparrec nparrec)
   in
-  ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), Declareops.no_seff
+  ([|fst ans (*FIXME*)|], Evd.empty_evar_universe_context (* FIXME *)), Declareops.no_seff
 
 let eq_dec_scheme_kind =
   declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 35ad31f0a6..b9c4a42943 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -294,14 +294,14 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 		  in obls, Some constr, typ
 		| None -> [||], None, termtype
 	      in
-	      let ctx = Evd.get_universe_context_set evm in
+	      let ctx = Evd.universe_context_set evm in
 		ignore (Obligations.add_definition id ?term:constr
 			typ ctx ~kind:(Global,poly,Instance) ~hook obls);
 		id
 	    else
 	      (Flags.silently 
 	       (fun () ->
-		Lemmas.start_proof id kind (termtype, Evd.get_universe_context_set evm)
+		Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm)
 		(fun _ -> instance_hook k pri global imps ?hook);
                  (* spiwack: I don't know what to do with the status here. *)
 		if not (Option.is_empty term) then 
@@ -335,7 +335,7 @@ let context l =
     with e when Errors.noncritical e ->
       error "Anonymous variables not allowed in contexts."
   in
-  let uctx = Evd.get_universe_context_set !evars in
+  let uctx = Evd.universe_context_set !evars in
   let fn status (id, b, t) =
     (* let uctx = Universes.shrink_universe_context uctx (Universes.universes_of_constr t) in *)
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 22830eb6df..4a26b75022 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -70,9 +70,9 @@ let red_constant_entry n ce = function
       let proof_out = ce.const_entry_body in
       let env = Global.env () in
       { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
-        (fun (body,eff) ->
-           under_binders env
-             (fst (reduction_of_red_expr env red)) n body,eff) }
+        (fun ((body,ctx),eff) ->
+          (under_binders env
+             (fst (reduction_of_red_expr env red)) n body,ctx),eff) }
 
 let interp_definition bl p red_option c ctypopt =
   let env = Global.env() in
@@ -90,7 +90,7 @@ let interp_definition bl p red_option c ctypopt =
         let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let vars = Universes.universes_of_constr body in
 	let ctx = Universes.restrict_universe_context
-	  (Evd.get_universe_context_set !evdref) vars in
+	  (Evd.universe_context_set !evdref) vars in
  	imps1@(Impargs.lift_implicits nb_args imps2),
 	  definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body
     | Some ctyp ->
@@ -116,7 +116,7 @@ let interp_definition bl p red_option c ctypopt =
         let vars = Univ.LSet.union (Universes.universes_of_constr body) 
           (Universes.universes_of_constr typ) in
         let ctx = Universes.restrict_universe_context
-          (Evd.get_universe_context_set !evdref) vars in
+          (Evd.universe_context_set !evdref) vars in
 	imps1@(Impargs.lift_implicits nb_args impsty),
 	  definition_entry ~types:typ ~poly:p 
 	    ~univs:(Univ.ContextSet.to_context ctx) body
@@ -171,8 +171,9 @@ let do_definition ident k bl red_option c ctypopt hook =
   let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
     if Flags.is_program_mode () then
       let env = Global.env () in
-      let c,sideff = Future.force ce.const_entry_body in
+      let (c,ctx), sideff = Future.force ce.const_entry_body in
       assert(Declareops.side_effects_is_empty sideff);
+      assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with 
 	| Some t -> t
 	| None -> Retyping.get_type_of env evd c
@@ -181,7 +182,7 @@ let do_definition ident k bl red_option c ctypopt hook =
       let obls, _, c, cty = 
 	Obligations.eterm_obligations env ident evd 0 c typ
       in
-      let ctx = Evd.get_universe_context_set evd in
+      let ctx = Evd.universe_context_set evd in
 	ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
       ignore(declare_definition ident k ce imps
@@ -228,7 +229,7 @@ let interp_assumption evdref env bl c =
   let c = prod_constr_expr c bl in
   let ty, impls = interp_type_evars_impls evdref env c in
   let evd, nf = nf_evars_and_universes !evdref in
-  let ctx = Evd.get_universe_context_set evd in
+  let ctx = Evd.universe_context_set evd in
     ((nf ty, ctx), impls)
 
 let declare_assumptions idl is_coe k c imps impl_is_on nl =
@@ -659,7 +660,7 @@ 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,eff) t imps =
+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)
 
@@ -873,7 +874,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let evars, _, evars_def, evars_typ = 
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
-  let ctx = Evd.get_universe_context_set !evdref in
+  let ctx = Evd.universe_context_set !evdref in
     ignore(Obligations.add_definition recname ~term:evars_def 
 	     evars_typ ctx evars ~hook)
 
@@ -939,12 +940,12 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
 let interp_fixpoint l ntns =
   let (env,_,evd),fix,info = interp_recursive true l ntns in
   check_recursive true env evd fix;
-  (fix,Evd.get_universe_context_set evd,info)
+  (fix,Evd.universe_context_set evd,info)
 
 let interp_cofixpoint l ntns =
   let (env,_,evd),fix,info = interp_recursive false l ntns in
   check_recursive false  env evd fix;
-  fix,Evd.get_universe_context_set evd,info
+  fix,Evd.universe_context_set evd,info
     
 let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
@@ -968,7 +969,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    let fixdecls = List.map (fun c -> c, Declareops.no_seff) fixdecls in
+    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
     ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
@@ -996,7 +997,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let fixdecls = List.map (fun c-> c,Declareops.no_seff) fixdecls in
+    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let ctx = Univ.ContextSet.to_context ctx in
     ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) 
@@ -1071,7 +1072,7 @@ let do_program_recursive local p fixkind fixl ntns =
 	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
 	List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
   end in
-  let ctx = Evd.get_universe_context_set evd in
+  let ctx = Evd.universe_context_set evd in
   let kind = match fixkind with
   | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
   | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5d0bcd78b6..3015eab25b 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -70,20 +70,17 @@ let abstract_inductive hyps nparams inds =
 
 let refresh_polymorphic_type_of_inductive (_,mip) =
   match mip.mind_arity with
-  | RegularArity s -> s.mind_user_arity, Univ.ContextSet.empty
+  | RegularArity s -> s.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
-    let univ, uctx = Universes.new_global_univ () in
-      mkArity (List.rev ctx, Type univ), uctx
+      mkArity (List.rev ctx, Type ar.template_level)
 
 let process_inductive (sechyps,abs_ctx) modlist mib =
   let nparams = mib.mind_nparams in
-  let univctx = ref Univ.ContextSet.empty in
   let inds =
     Array.map_to_list
       (fun mip ->
-	let ty, uctx = refresh_polymorphic_type_of_inductive (mib,mip) in
-	let () = univctx := Univ.ContextSet.union uctx !univctx in
+	let ty = refresh_polymorphic_type_of_inductive (mib,mip) in
 	let arity = expmod_constr modlist ty in
 	let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
 	  (mip.mind_typename,
@@ -93,10 +90,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
       mib.mind_packets in
   let sechyps' = map_named_context (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
-  let univs = Univ.UContext.union abs_ctx 
-    (Univ.UContext.union (Univ.ContextSet.to_context !univctx) 
-       mib.mind_universes)
-  in
+  let univs = Univ.UContext.union abs_ctx mib.mind_universes in
   { mind_entry_record = mib.mind_record <> None;
     mind_entry_finite = mib.mind_finite;
     mind_entry_params = params';
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 2a408e03d1..1ee2adcd8c 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -123,7 +123,7 @@ let define internal id c p univs =
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
   let entry = {
-    const_entry_body = Future.from_val (c,Declareops.no_seff);
+    const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
     const_entry_secctx = None;
     const_entry_type = None;
     const_entry_proj = None;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 57b428b5cd..ac3bf59295 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -361,7 +361,7 @@ let do_mutual_induction_scheme lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma decl in
     (* let decltype = refresh_universes decltype in *)
-    let proof_output = Future.from_val (decl,Declareops.no_seff) in
+    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in
     let cst = define fi UserVerbose sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
@@ -459,7 +459,7 @@ let do_combined_scheme name schemes =
       schemes
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val (body,Declareops.no_seff) in
+  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in
   ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ));
   fixpoint_message None [snd name]
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 97c95bfd86..d45c2af3ed 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -560,6 +560,8 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
       let ctx = fst (decompose_prod_n_assum m fixtype) in
 	List.map_i (fun i _ -> i) 0 ctx
 
+let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff)
+
 let declare_mutual_definition l =
   let len = List.length l in
   let first = List.hd l in
@@ -589,11 +591,11 @@ let declare_mutual_definition l =
               possible_indexes fixdecls in
           Some indexes, 
           List.map_i (fun i _ ->
-            mkFix ((indexes,i),fixdecls),Declareops.no_seff) 0 l
+            mk_proof (mkFix ((indexes,i),fixdecls))) 0 l
       | IsCoFixpoint ->
           None,
           List.map_i (fun i _ ->
-            mkCoFix (i,fixdecls),Declareops.no_seff) 0 l
+            mk_proof (mkCoFix (i,fixdecls))) 0 l
   in
   (* Declare the recursive definitions *)
   let ctx = Univ.ContextSet.to_context first.prg_ctx in
@@ -630,7 +632,7 @@ let declare_obligation prg obl body uctx =
 	  shrink_body body else [], body, [||] 
       in
       let ce = 
-        { const_entry_body = Future.from_val(body,Declareops.no_seff);
+        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then Some ty else None;
 	  const_entry_proj = None;
@@ -796,8 +798,8 @@ let solve_by_tac name evi t poly subst ctx =
   let entry = Term_typing.handle_side_effects env entry in
   let body, eff = Future.force entry.Entries.const_entry_body in
   assert(Declareops.side_effects_is_empty eff);
-  Inductiveops.control_only_guard (Global.env ()) body;
-  body, subst, entry.Entries.const_entry_universes
+  Inductiveops.control_only_guard (Global.env ()) (fst body) (*FIXME ignoring the context...*);
+  (fst body), subst, entry.Entries.const_entry_universes
 
   (* try *)
   (*   let substref = ref (Univ.LMap.empty, Univ.UContext.empty) in *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index af7f364f31..c4a4951b3c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -258,7 +258,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 		  in
 		  let cie = {
                     const_entry_body =
-                      Future.from_val (proj,Declareops.no_seff);
+                      Future.from_val (Term_typing.mk_pure_proof proj);
                     const_entry_secctx = None;
                     const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ca31d1f2ed..0dbc77b83e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1411,11 +1411,12 @@ let vernac_declare_reduction locality s r =
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
-  let evmap = Evd.empty in
   let env = Global.env() in
+  let evmap = Evd.from_env env in
   let c,ctx = interp_constr evmap env c in
   let senv = Global.safe_env() in
-  let senv = Safe_typing.add_constraints (snd ctx) senv in
+  let cstrs = snd (Evd.evar_universe_context_set ctx) in
+  let senv = Safe_typing.add_constraints cstrs senv in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
     msg_notice (print_safe_judgment env j)