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/Machconcr.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/Machconcr.v')
| -rw-r--r-- | backend/Machconcr.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 4417cc6f..876f558c 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -86,7 +86,7 @@ Definition extcall_arguments (** Mach execution states. *) -Inductive stackframe: Set := +Inductive stackframe: Type := | Stackframe: forall (f: block) (**r pointer to calling function *) (sp: val) (**r stack pointer in calling function *) @@ -94,7 +94,7 @@ Inductive stackframe: Set := (c: code), (**r program point in calling function *) stackframe. -Inductive state: Set := +Inductive state: Type := | State: forall (stack: list stackframe) (**r call stack *) (f: block) (**r pointer to current function *) |