Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 16 insertions, 23 deletions

diff --git a/lib/Intv.v b/lib/Intv.v
index 834f83d..a8fbd71 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -248,16 +248,13 @@ Next Obligation.
   destruct H2. congruence. auto. 
 Qed.
 Next Obligation.
-  elim wildcard'0. intros y [A B]. exists y; split; auto. omega.
+  exists wildcard'0; split; auto. omega.
 Qed.
 Next Obligation.
   exists (hi - 1); split; auto. omega.
 Qed.
 Next Obligation.
   omegaContradiction.
-Qed.
-Next Obligation.
-  apply Zwf_well_founded.
 Defined.
 
 End FORALL.
diff --git a/lib/Lattice.v b/lib/Lattice.v
index c200fc8..51a7976 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -64,11 +64,11 @@ Set Implicit Arguments.
 
 Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP.
 
-Inductive t_ : Type :=
-  | Bot_except: PTree.t L.t -> t_
-  | Top_except: PTree.t L.t -> t_.
+Inductive t' : Type :=
+  | Bot_except: PTree.t L.t -> t'
+  | Top_except: PTree.t L.t -> t'.
 
-Definition t: Type := t_.
+Definition t: Type := t'.
 
 Definition get (p: positive) (x: t) : L.t :=
   match x with
@@ -611,12 +611,12 @@ End LFSet.
 
 Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP.
 
-Inductive t_ : Type :=
-  | Bot: t_
-  | Inj: X.t -> t_
-  | Top: t_.
+Inductive t' : Type :=
+  | Bot: t'
+  | Inj: X.t -> t'
+  | Top: t'.
 
-Definition t : Type := t_.
+Definition t : Type := t'.
 
 Definition eq (x y: t) := (x = y).
 Definition eq_refl: forall x, eq x x := (@refl_equal t).
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 493b0bd..fb04310 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -1017,7 +1017,7 @@ Lemma split_move_charact:
 Proof.
   unfold no_read. intros m r. functional induction (split_move m r).
   red; simpl. tauto.
-  rewrite _x. split. reflexivity. simpl;auto.
+  split. reflexivity. simpl; auto.
   rewrite e1 in IHo. simpl. intuition.
   rewrite e1 in IHo. destruct IHo. split. rewrite H. reflexivity.
   simpl. intuition.
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index d74a20a..553d905 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -635,26 +635,22 @@ Next Obligation.
   red. auto.
 Qed.
 Next Obligation.
-  destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
-                   (find_x_obligation_1 a find_x a' Heq_anonymous)))
+  (* a <> b*)
+  destruct (find_x a')
   as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
   apply repr_some_diff. auto.
 Qed.
 Next Obligation.
-  destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
-                   (find_x_obligation_1 a find_x a' Heq_anonymous)))
-  as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
+  destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
   rewrite B. apply repr_some. auto.
 Qed.
 Next Obligation.
   split.
-  destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
-                   (find_x_obligation_1 a find_x a' Heq_anonymous)))
+  destruct (find_x a')
   as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
   symmetry. apply repr_some. auto.
   intros. rewrite repr_compress. 
-  destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
-                   (find_x_obligation_1 a find_x a' Heq_anonymous)))
+  destruct (find_x a')
   as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto.
 Qed.
 Next Obligation.