Adapted to work with Coq 8.2-1v1.4.1

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

1 files changed, 5 insertions, 5 deletions

diff --git a/backend/Kildall.v b/backend/Kildall.v
index b4445aeb..188a23fd 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -108,7 +108,7 @@ End DATAFLOW_SOLVER.
 
 Module Type NODE_SET.
 
-  Variable t: Set.
+  Variable t: Type.
   Variable add: positive -> t -> t.
   Variable pick: t -> option (positive * t).
   Variable initial: positive -> t.
@@ -147,7 +147,7 @@ Variable entrypoints: list (positive * L.t).
 - A worklist of program points that remain to be considered.
 *)
 
-Record state : Set :=
+Record state : Type :=
   mkstate { st_in: PMap.t L.t; st_wrk: NS.t }.
 
 (** Kildall's algorithm, in pseudo-code, is as follows:
@@ -663,7 +663,7 @@ End Backward_Dataflow_Solver.
 
 Module Type ORDERED_TYPE_WITH_TOP.
 
-  Variable t: Set.
+  Variable t: Type.
   Variable ge: t -> t -> Prop.
   Variable top: t.
   Hypothesis top_ge: forall x, ge top x.
@@ -736,7 +736,7 @@ Definition result := PMap.t L.t.
 - A worklist of program points that remain to be considered.
 *)
 
-Record state : Set := mkstate
+Record state : Type := mkstate
   { st_in: result; st_wrk: list positive }.
 
 (** The ``extended basic block'' algorithm, in pseudo-code, is as follows:
@@ -1167,7 +1167,7 @@ Module NodeSetForward <: NODE_SET.
     rewrite positive_rec_succ. rewrite PositiveSetFacts.add_iff. 
     elim (Plt_succ_inv _ _ H0); intro.
     right. apply H. auto.
-    left. red. red. auto.
+    left. auto.
   Qed.
 End NodeSetForward.