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 /driver/Compiler.v | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
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
Diffstat (limited to 'driver/Compiler.v')
| -rw-r--r-- | driver/Compiler.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index bce0dab..97bc19b 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -80,10 +80,10 @@ Open Local Scope string_scope. (** We first define useful monadic composition operators, along with funny (but convenient) notations. *) -Definition apply_total (A B: Set) (x: res A) (f: A -> B) : res B := +Definition apply_total (A B: Type) (x: res A) (f: A -> B) : res B := match x with Error msg => Error msg | OK x1 => OK (f x1) end. -Definition apply_partial (A B: Set) +Definition apply_partial (A B: Type) (x: res A) (f: A -> res B) : res B := match x with Error msg => Error msg | OK x1 => f x1 end. @@ -150,7 +150,7 @@ Definition transf_c_program (p: Csyntax.program) : res Asm.program := (** The following lemmas help reason over compositions of passes. *) Lemma map_partial_compose: - forall (X A B C: Set) + forall (X A B C: Type) (ctx: X -> errmsg) (f1: A -> res B) (f2: B -> res C) (pa: list (X * A)) (pc: list (X * C)), @@ -168,7 +168,7 @@ Proof. Qed. Lemma transform_partial_program_compose: - forall (A B C V: Set) + forall (A B C V: Type) (f1: A -> res B) (f2: B -> res C) (pa: program A V) (pc: program C V), transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> @@ -183,7 +183,7 @@ Proof. Qed. Lemma transform_program_partial_program: - forall (A B V: Set) (f: A -> B) (p: program A V) (tp: program B V), + forall (A B V: Type) (f: A -> B) (p: program A V) (tp: program B V), transform_partial_program (fun x => OK (f x)) p = OK tp -> transform_program f p = tp. Proof. @@ -192,7 +192,7 @@ Proof. Qed. Lemma transform_program_compose: - forall (A B C V: Set) + forall (A B C V: Type) (f1: A -> res B) (f2: B -> C) (pa: program A V) (pc: program C V), transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> @@ -209,7 +209,7 @@ Proof. Qed. Lemma transform_partial_program_identity: - forall (A V: Set) (pa pb: program A V), + forall (A V: Type) (pa pb: program A V), transform_partial_program (@OK A) pa = OK pb -> pa = pb. Proof. |