- 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, 112 insertions, 64 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0f296c6af0..ab2a165757 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 *)
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 328d45991b..96258a84bc 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -125,7 +125,7 @@ let e_exact poly flags (c,clenv) =
   let clenv', subst = 
     if poly then Clenv.refresh_undefined_univs clenv 
     else clenv, Univ.empty_level_subst
-  in e_give_exact ~flags (Vars.subst_univs_level_constr subst c)
+  in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
     
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index eb8d27f253..e91c212933 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1371,7 +1371,10 @@ let swapEquandsInConcl =
   let (lbeq,u,eq_args) = find_eq_data (pf_nf_concl gl) in
   let args = swap_equality_args eq_args @ [Evarutil.mk_new_meta ()] in
     pf_constr_of_global lbeq.sym (fun sym_equal ->
-      Proofview.V82.tactic (refine (applist (sym_equal, args))))
+      Proofview.V82.tactic (fun gls ->
+	let c = applist (sym_equal, args) in
+	let sigma, cty = pf_apply Typing.e_type_of gl c in
+	  refine (applist (c,[Evarutil.mk_new_meta()])) {gls with sigma}))
   end
 
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
@@ -1383,10 +1386,12 @@ let bareRevSubstInConcl (lbeq,u) body (t,e1,e2) =
   let eq_elim, effs = find_elim eq (Some false) false None None gl in
   (* build substitution predicate *)
   let p = lambda_create (Proofview.Goal.env gl) (t,body) in
+  let sigma, pty = pf_apply Typing.e_type_of gl p in
   (* apply substitution scheme *)
   let args = [t; e1; p; Evarutil.mk_new_meta (); e2; Evarutil.mk_new_meta ()] in
-    pf_constr_of_global (ConstRef eq_elim) (fun c ->
-      Proofview.V82.tactic (refine (applist (c, args))))
+    Proofview.V82.tclEVARS sigma <*>
+      (pf_constr_of_global (ConstRef eq_elim) (fun c ->
+	Proofview.V82.tactic (refine (applist (c, args)))))
   end
 
 (* [subst_tuple_term dep_pair B]
@@ -1456,7 +1461,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let expected_goal = beta_applist (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
-    pred_body,expected_goal
+  (* Retype to get universes right *)
+  let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in
+    sigma,pred_body,expected_goal
 
 (* Like "replace" but decompose dependent equalities *)
 
@@ -1466,11 +1473,12 @@ let cutSubstInConcl_RL eqn =
   Proofview.Goal.raw_enter begin fun gl ->
   let (lbeq,u,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in
   let concl = pf_nf_concl gl in
-  let body,expected_goal = pf_apply subst_tuple_term gl e2 e1 concl in
+  let sigma,body,expected_goal = pf_apply subst_tuple_term gl e2 e1 concl in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
-  tclTHENFIRST
-    (bareRevSubstInConcl (lbeq,u) body eq)
-    (Proofview.V82.tactic (fun gl -> convert_concl expected_goal DEFAULTcast gl))
+    Proofview.V82.tclEVARS sigma <*>
+      tclTHENFIRST
+      (bareRevSubstInConcl (lbeq,u) body eq)
+      (Proofview.V82.tactic (fun gl -> convert_concl expected_goal DEFAULTcast gl))
   end
 
 (* |- (P e1)
@@ -1488,11 +1496,12 @@ let cutSubstInHyp_LR eqn id =
   Proofview.Goal.enter begin fun gl ->
   let (lbeq,u,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in
   let idtyp = pf_get_hyp_typ id gl in
-  let body,expected_goal = pf_apply subst_tuple_term gl e1 e2 idtyp in
+  let sigma,body,expected_goal = pf_apply subst_tuple_term gl e1 e2 idtyp in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
   let refine = Proofview.V82.tactic (fun gl -> Tacmach.refine_no_check (mkVar id) gl) in
   let subst = Proofview.V82.of_tactic (tclTHENFIRST (bareRevSubstInConcl (lbeq,u) body eq) refine) in
-  Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal subst gl)
+    Proofview.V82.tclEVARS sigma <*>
+      Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal subst gl)
   end
 
 let cutSubstInHyp_RL eqn id =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bda217566d..e87c665d09 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -256,8 +256,11 @@ let add_rewrite_hint bases ort t lcsr =
   let f ce = 
     let c, ctx = Constrintern.interp_constr sigma env ce in
     let ctx =
-      if poly then ctx
-      else (Global.add_constraints (snd ctx); Univ.ContextSet.empty)
+      if poly then 
+	Evd.evar_universe_context_set ctx
+      else 
+	let cstrs = Evd.evar_universe_context_constraints ctx in
+	  (Global.add_constraints cstrs; Univ.ContextSet.empty)
     in
       Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in
   let eqs = List.map f lcsr in
@@ -619,7 +622,7 @@ let hResolve id c occ t gl =
           resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
   in
   let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
-  let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
+  let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
     tclTHEN (Refiner.tclEVARS sigma)
      (change_in_concl None (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl))) gl
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 81bc6a256c..a10ad1e2bc 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     errorlabstrm "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let pf = Proof.start Evd.empty [invEnv,(invGoal,get_universe_context_set sigma)] in
+  let pf = Proof.start Evd.empty [invEnv,(invGoal,universe_context_set sigma)] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
@@ -236,10 +236,9 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
 
 let add_inversion_lemma_exn na com comsort bool tac =
-  let env = Global.env () and sigma = Evd.empty in
-  let c,ctx = Constrintern.interp_type sigma env com in
-  let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
-  let sigma, sort = Pretyping.interp_sort sigma comsort in
+  let env = Global.env () and evd = ref Evd.empty in
+  let c = Constrintern.interp_type_evars evd env com in
+  let sigma, sort = Pretyping.interp_sort !evd comsort in
   try
     add_inversion_lemma na env sigma c sort bool tac
   with
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index cbf33fdb44..c6c4049923 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -587,7 +587,7 @@ let solve_remaining_by by env prf =
       List.fold_right (fun mv evd ->
         let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
 	let c,_,_ = Pfedit.build_by_tactic env.env (ty,Univ.ContextSet.empty) (Tacticals.New.tclCOMPLETE tac) in
-	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
+	  meta_assign mv (fst c (*FIXME*), (Conv,TypeNotProcessed)) evd)
       indep env.evd
     in { env with evd = evd' }, prf
 
@@ -1526,7 +1526,8 @@ let newtactic_init_setoid () =
   with e when Errors.noncritical e -> Proofview.tclZERO e
 
 let tactic_init_setoid () = 
-  init_setoid (); tclIDTAC
+  try init_setoid (); tclIDTAC
+  with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
   
 let cl_rewrite_clause_new_strat ?abs strat clause =
   Proofview.tclTHEN (newtactic_init_setoid ())
@@ -1534,10 +1535,9 @@ let cl_rewrite_clause_new_strat ?abs strat clause =
    with RewriteFailure s ->
    newfail 0 (str"setoid rewrite failed: " ++ s))
 
-(* let cl_rewrite_clause_newtac' l left2right occs clause = *)
-(*   Proof_global.run_tactic  *)
-(*     (Proofview.tclFOCUS 1 1  *)
-(*        (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)) *)
+let cl_rewrite_clause_newtac' l left2right occs clause =
+  Proofview.tclFOCUS 1 1
+    (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)
 
 let cl_rewrite_clause_strat strat clause =
   tclTHEN (tactic_init_setoid ())
@@ -1765,7 +1765,7 @@ let declare_projection n instance_id r =
 let build_morphism_signature m =
   let env = Global.env () in
   let m,ctx = Constrintern.interp_constr Evd.empty env m in
-  let sigma = Evd.from_env ~ctx env in
+  let sigma = Evd.from_env ~ctx:(Evd.evar_universe_context_set ctx) env in
   let t = Typing.type_of env sigma m in
   let cstrs =
     let rec aux t =
@@ -1969,12 +1969,15 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
 		  (pf_env gl,project gl,
 		  Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl)))
 
+open Proofview.Notations
+
 let general_s_rewrite_clause x =
-  init_setoid ();
-  fun b occs cl ~new_goals ->
   match x with
-    | None -> Proofview.V82.tactic (general_s_rewrite None b occs cl ~new_goals)
-    | Some id -> Proofview.V82.tactic (general_s_rewrite (Some id) b occs cl ~new_goals)
+    | None -> general_s_rewrite None
+    | Some id -> general_s_rewrite (Some id)
+let general_s_rewrite_clause x y z w ~new_goals =
+  newtactic_init_setoid () <*>
+  Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals)
 
 let _ = Hook.set Equality.general_rewrite_clause general_s_rewrite_clause
 
@@ -1989,25 +1992,39 @@ let setoid_proof ty fn fallback =
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let concl = Proofview.Goal.concl gl in
-    try
-      let rel, args = decompose_app_rel env sigma concl in
-      let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env sigma rel)))) in
-      Proofview.V82.tactic (fn env sigma car rel)
-    with e when Errors.noncritical e ->
-      Proofview.tclORELSE fallback (function
-      | Hipattern.NoEquationFound ->
-          let e = Errors.push e in
-	  begin match e with
-	  | Not_found ->
-	      let rel, args = decompose_app_rel env sigma concl in
-		not_declared env ty rel
-	  | _ -> raise e
-          end
-      | e -> Proofview.tclZERO e)
+    Proofview.tclORELSE
+      begin
+        try
+          let rel, args = decompose_app_rel env sigma concl in
+          let evm = sigma in
+          let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
+          fn env sigma car rel
+        with e -> Proofview.tclZERO e
+      end
+      begin function
+        | e ->
+            Proofview.tclORELSE
+              fallback
+              begin function
+                | Hipattern.NoEquationFound ->
+                (* spiwack: [Errors.push] here is unlikely to do what
+                   it's intended to, or anything meaningful for that
+                   matter. *)
+                    let e = Errors.push e in
+	            begin match e with
+	            | Not_found ->
+	                let rel, args = decompose_app_rel env sigma concl in
+		        not_declared env ty rel
+	            | _ -> Proofview.tclZERO e
+                    end
+                | e' -> Proofview.tclZERO e'
+              end
+      end
   end
 
 let tac_open ((evm,_), c) tac = 
-  tclTHEN (Refiner.tclEVARS evm) (tac c)
+  Proofview.V82.tactic 
+    (tclTHEN (Refiner.tclEVARS evm) (tac c))
 
 let poly_proof getp gett env evm car rel =
   if Sorts.is_prop (sort_of_rel env evm rel) then
@@ -2024,18 +2041,20 @@ let setoid_reflexivity =
 let setoid_symmetry =
   setoid_proof "symmetric"
     (fun env evm car rel -> 
-      tac_open (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
-		  env evm car rel) apply)
+      tac_open
+	(poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
+	   env evm car rel)
+	apply)
     (symmetry_red true)
-
+    
 let setoid_transitivity c =
   setoid_proof "transitive"
     (fun env evm car rel ->
-      let proof = poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
-	env evm car rel in
-	match c with
-	| None -> tac_open proof eapply
-	| Some c -> tac_open proof (fun t -> apply_with_bindings (t,ImplicitBindings [ c ])))
+      tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
+	   env evm car rel)
+	(fun proof -> match c with
+	| None -> eapply proof
+	| Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 9bdfc08d2e..0f155c8bb8 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -41,6 +41,10 @@ val cl_rewrite_clause :
   interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
   bool -> Locus.occurrences -> Id.t option -> tactic
 
+val cl_rewrite_clause_newtac' :
+  interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
+  bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
+
 val is_applied_rewrite_relation :
   env -> evar_map -> Context.rel_context -> constr -> types option
 
@@ -57,6 +61,12 @@ val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
 val add_morphism :
   bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit
 
+val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
+
+val get_symmetric_proof : env -> evar_map -> constr -> constr -> evar_map * constr
+
+val get_transitive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
+
 val default_morphism :
   (types * constr option) option list * (types * types option) option ->
   constr -> constr * constr
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 128d8ea87e..f32c06ba40 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2145,7 +2145,7 @@ let _ =
     if has_type arg (glbwit wit_tactic) then
       let tac = out_gen (glbwit wit_tactic) arg in
       let tac = interp_tactic ist tac in
-      let ctx = Evd.get_universe_context_set sigma in
+      let ctx = Evd.universe_context_set sigma in
       let prf = Proof.start sigma [env, (ty, ctx)] in
       let (prf, _) =
         try Proof.run_tactic env tac prf
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cc1096e7ca..024165fd02 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1224,7 +1224,7 @@ let vm_cast_no_check c gl =
 
 let exact_proof c gl =
   let c,ctx = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
-  in tclPUSHCONTEXT Evd.univ_flexible ctx (refine_no_check c) gl
+  in tclTHEN (tclPUSHEVARUNIVCONTEXT ctx) (refine_no_check c) gl
 
 let assumption =
   let rec arec gl only_eq = function
@@ -1237,12 +1237,14 @@ let assumption =
     let concl = Proofview.Goal.concl gl in
     let sigma = Proofview.Goal.sigma gl in
     let (sigma, is_same_type) =
-      if only_eq then (sigma, eq_constr t concl)
+      if only_eq then (sigma, Constr.equal t concl)
       else
         let env = Proofview.Goal.env gl in
         infer_conv env sigma t concl
     in
-    if is_same_type then Proofview.Refine.refine (fun h -> (h, mkVar id))
+    if is_same_type then 
+	(Proofview.V82.tclEVARS sigma) <*> 
+	  Proofview.Refine.refine (fun h -> (h, mkVar id))
     else arec gl only_eq rest
   in
   let assumption_tac gl =
@@ -3743,7 +3745,7 @@ let abstract_subproof id tac =
   let evd, ctx, concl = 
     (* FIXME: should be done only if the tactic succeeds *)
     let evd, nf = nf_evars_and_universes (Proofview.Goal.sigma gl) in
-    let ctx = Evd.get_universe_context_set evd in
+    let ctx = Evd.universe_context_set evd in
       evd, ctx, nf concl
   in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in