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/CminorSel.v | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
| download | compcert-kvx-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.tar.gz compcert-kvx-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/CminorSel.v')
| -rw-r--r-- | backend/CminorSel.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/backend/CminorSel.v b/backend/CminorSel.v index bfe92a40..1e798b5f 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -40,7 +40,7 @@ Require Import Smallstep. boolean value only and not their exact value. *) -Inductive expr : Set := +Inductive expr : Type := | Evar : ident -> expr | Eop : operation -> exprlist -> expr | Eload : memory_chunk -> addressing -> exprlist -> expr @@ -48,13 +48,13 @@ Inductive expr : Set := | Elet : expr -> expr -> expr | Eletvar : nat -> expr -with condexpr : Set := +with condexpr : Type := | CEtrue: condexpr | CEfalse: condexpr | CEcond: condition -> exprlist -> condexpr | CEcondition : condexpr -> condexpr -> condexpr -> condexpr -with exprlist : Set := +with exprlist : Type := | Enil: exprlist | Econs: expr -> exprlist -> exprlist. @@ -62,7 +62,7 @@ with exprlist : Set := if/then/else conditional is a [condexpr], and the [Sstore] construct uses a machine-dependent addressing mode. *) -Inductive stmt : Set := +Inductive stmt : Type := | Sskip: stmt | Sassign : ident -> expr -> stmt | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt @@ -78,7 +78,7 @@ Inductive stmt : Set := | Slabel: label -> stmt -> stmt | Sgoto: label -> stmt. -Record function : Set := mkfunction { +Record function : Type := mkfunction { fn_sig: signature; fn_params: list ident; fn_vars: list ident; @@ -108,7 +108,7 @@ Definition letenv := list val. (** Continuations *) -Inductive cont: Set := +Inductive cont: Type := | Kstop: cont (**r stop program execution *) | Kseq: stmt -> cont -> cont (**r execute stmt, then cont *) | Kblock: cont -> cont (**r exit a block, then do cont *) @@ -117,7 +117,7 @@ Inductive cont: Set := (** States *) -Inductive state: Set := +Inductive state: Type := | State: (**r execution within a function *) forall (f: function) (**r currently executing function *) (s: stmt) (**r statement under consideration *) |