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/LTLin.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'backend/LTLin.v') diff --git a/backend/LTLin.v b/backend/LTLin.v index 4c87c0d6..10b7d832 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -41,7 +41,7 @@ Definition label := positive. transfer control to the given code label. Labels are explicitly inserted in the instruction list as pseudo-instructions [Llabel]. *) -Inductive instruction: Set := +Inductive instruction: Type := | Lop: operation -> list loc -> loc -> instruction | Lload: memory_chunk -> addressing -> list loc -> loc -> instruction | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction @@ -52,9 +52,9 @@ Inductive instruction: Set := | Lcond: condition -> list loc -> label -> instruction | Lreturn: option loc -> instruction. -Definition code: Set := list instruction. +Definition code: Type := list instruction. -Record function: Set := mkfunction { +Record function: Type := mkfunction { fn_sig: signature; fn_params: list loc; fn_stacksize: Z; @@ -109,7 +109,7 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := code sequences [c] (suffixes of the code of the current function). *) -Inductive stackframe : Set := +Inductive stackframe : Type := | Stackframe: forall (res: loc) (**r where to store the result *) (f: function) (**r calling function *) @@ -118,7 +118,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: function) (**r function currently executing *) -- cgit