- 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

6 files changed, 14 insertions, 49 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 783abc5d8d..b85b7995cb 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -395,7 +395,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let neweq=new_app_global _eq [|intype;t1;t2|] in
     Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evm)
       (Tacticals.New.tclTHENS (neweq (assert_tac (Name hid)))
-        [proof_tac p; Proofview.V82.tactic (endt exact_check)])
+        [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
   end
 
 (* wrap everything *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8a9c7d2e7b..a8876c75b1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -554,7 +554,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
     let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
-    let ctxt,fix = decompose_lam_assum (fst(Future.force first_princ_body)) in (* the principle has for forall ...., fix .*)
+    let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
       List.map (* we can now compute the other principles *)
@@ -597,7 +597,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	   in
 	   {const with
 	      Entries.const_entry_body = 
-                (Future.from_val (princ_body,Declareops.no_seff));
+                (Future.from_val (Term_typing.mk_pure_proof princ_body));
 	      Entries.const_entry_type = Some scheme_type
 	   }
       )
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b68d9762ef..072b1ce005 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1059,7 +1059,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	  Array.of_list
 	    (List.map
 	       (fun entry ->
-		  (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type )
+		  (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type )
 	       )
 	       (make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
 	    )
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8496bbbb35..4390143619 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1376,7 +1376,7 @@ let com_terminate
   start_proof ctx tclIDTAC tclIDTAC;
   try
     let sigma, new_goal_type = build_new_goal_type () in
-    open_new_goal start_proof (Evd.get_universe_context_set sigma)
+    open_new_goal start_proof (Evd.universe_context_set sigma)
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type);
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 689462704c..3fa9e02cff 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -210,10 +210,15 @@ let rec mk_nat = function
 
 (* Lists *)
 
-let mkListConst c u = 
-  Term.mkConstructU (Globnames.destConstructRef 
-		     (Coqlib.gen_reference "" ["Init";"Datatypes"] c),
-		     Univ.Instance.of_array [|u|])
+let mkListConst c = 
+  let r = 
+    Coqlib.gen_reference "" ["Init";"Datatypes"] c
+  in 
+  let inst = 
+    if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|]
+    else fun _ -> Univ.Instance.empty
+  in
+    fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u)
 
 let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|])
 let coq_nil univ typ =  Term.mkApp (mkListConst "nil" univ, [|typ|])
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index de308c2964..85fd810264 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -113,28 +113,6 @@ Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef.
 Proof.
 generalize (CRmorph.(morph_eq) c c').
 destruct (c =? c')%coef; auto.
-<<<<<<< HEAD
-=======
-||||||| merged common ancestors
-destruct (c ?= c')%coef; auto.
-=======
-destruct (c ?= c')%coef; auto.
-<<<<<<< HEAD
-=======
-intros.
-generalize (fun h => X (morph_eq CRmorph _ _ h)).
-case (ceqb c1 c2); auto.
->>>>>>> .merge_file_U4r9lJ
->>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
-||||||| merged common ancestors
-=======
-intros.
-generalize (fun h => X (morph_eq CRmorph _ _ h)).
-case (ceqb c1 c2); auto.
->>>>>>> .merge_file_U4r9lJ
-=======
->>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
->>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
 Qed.
 
 (* Power coefficients : Cpow *)
@@ -301,24 +279,6 @@ apply radd_ext.
   [ ring | now rewrite rdiv_simpl ].
 Qed.
 
-<<<<<<< HEAD
-Theorem rdiv3 r1 r2 r3 r4 :
- ~ r2 == 0 ->
- ~ r4 == 0 ->
- r1 / r2 - r3 / r4 == (r1 * r4 -  r3 * r2) / (r2 * r4).
-Proof.
-intros H2 H4.
-assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
-transitivity (r1 / r2 + - (r3 / r4)); auto.
-transitivity (r1 / r2 + - r3 / r4); auto.
-transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)).
-apply rdiv2; auto.
-f_equiv.
-transitivity (r1 * r4 + - (r3 * r2)); auto.
-Qed.
-
-=======
->>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
 Theorem rdiv5 a b : - (a / b) == - a / b.
 Proof.
 now rewrite !rdiv_def, ropp_mul_l.