From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 5 Jun 2009 13:39:59 +0000 Subject: 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 --- backend/Machconcr.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/Machconcr.v') 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 *) -- cgit