diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
commit | 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 (patch) | |
tree | ec5f45b6546e19519f59b1ee0f42955616ca1b98 /backend/Kildall.v | |
parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
download | compcert-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.tar.gz compcert-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.zip |
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
Diffstat (limited to 'backend/Kildall.v')
-rw-r--r-- | backend/Kildall.v | 10 |
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. |