From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 5 Jun 2009 13:39:59 +0000 Subject: Adapted to work with Coq 8.2-1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Kildall.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'backend/Kildall.v') 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. -- cgit