Correct rebase on STM code. Thanks to E. Tassi for help on dealing with

latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.

- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-

5 files changed, 6 insertions, 6 deletions

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index d75eb384f6..ba62fa7fd5 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -125,7 +125,6 @@ Proof.
  intros x y z H; revert z; induction H; auto.
  inversion 1; subst; auto. invlist eqlistA; eauto with *.
 Qed.
-
 (** Moreover, [eqlistA] implies [equivlistA]. A reverse result
     will be proved later for sorted list without duplicates. *)
 
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 4a4fc23f94..76f8a55a42 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -42,8 +42,8 @@ intros A B.
 apply (dependent_unique_choice A (fun _ => B)).
 Qed.
 
-(** The following proof comes from [[ChicliPottierSimpson02]] *)
 
+(** The following proof comes from [[ChicliPottierSimpson02]] *)
 Require Import Setoid.
 
 Theorem classic_set_in_prop_context :
@@ -78,7 +78,7 @@ destruct (f P).
   right.
   destruct HfP as [[_ Hfalse]| [Hna _]].
     discriminate.
-    assumption.
+    assumption. 
 Qed.
 
 Corollary not_not_classic_set :
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 3142d97ca9..6164e6e93e 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -962,7 +962,8 @@ Proof. firstorder. Qed.
 Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s').
 Proof.
  unfold eq, Equal, L.eq; intros.
- setoid_rewrite elements_spec1; firstorder.
+ do 2 setoid_rewrite elements_spec1. (*FIXME due to regression in rewrite *) 
+ firstorder. 
 Qed.
 
 Definition lt (s1 s2 : tree) : Prop :=
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index b444d443d0..acc9fd5d64 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -812,7 +812,7 @@ Hint Resolve Rinv_involutive: real.
 Lemma Rinv_mult_distr :
   forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2.
 Proof.
-  intros; field; auto.
+  intros; field; auto.  
 Qed.
 
 (*********)
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index a89b90238e..5b52c6ec9b 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -69,7 +69,7 @@ Section defs.
       (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) ->
       forall l:list A, Sorted l -> P l.
   Proof.
-    induction l; firstorder using Sorted_inv.
+    induction l. firstorder using Sorted_inv. firstorder using Sorted_inv.
   Qed.
 
   Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l.