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 /lib/Iteration.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 'lib/Iteration.v')
| -rw-r--r-- | lib/Iteration.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/Iteration.v b/lib/Iteration.v index cabe5b82..24835da2 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -18,9 +18,9 @@ Require Import Max. Module Type ITER. Variable iterate - : forall A B : Set, (A -> B + A) -> A -> option B. + : forall A B : Type, (A -> B + A) -> A -> option B. Hypothesis iterate_prop - : forall (A B : Set) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop), + : forall (A B : Type) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop), (forall a : A, P a -> match step a with inl b => Q b | inr a' => P a' end) -> forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b. @@ -39,7 +39,7 @@ Module PrimIter: ITER. Section ITERATION. -Variables A B: Set. +Variables A B: Type. Variable step: A -> B + A. (** The [step] parameter represents one step of the iteration. From a @@ -174,7 +174,7 @@ Module GenIter: ITER. Section ITERATION. -Variables A B: Set. +Variables A B: Type. Variable step: A -> B + A. Definition B_le (x y: option B) : Prop := x = None \/ y = x. |