From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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/Linear.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'backend/Linear.v')

diff --git a/backend/Linear.v b/backend/Linear.v
index 34d6e5ce..e025407a 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -35,7 +35,7 @@ Require Import Conventions.
 
 Definition label := positive.
 
-Inductive instruction: Set :=
+Inductive instruction: Type :=
   | Lgetstack: slot -> mreg -> instruction
   | Lsetstack: mreg -> slot -> instruction
   | Lop: operation -> list mreg -> mreg -> instruction
@@ -48,9 +48,9 @@ Inductive instruction: Set :=
   | Lcond: condition -> list mreg -> label -> instruction
   | Lreturn: instruction.
 
-Definition code: Set := list instruction.
+Definition code: Type := list instruction.
 
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
   fn_sig: signature;
   fn_stacksize: Z;
   fn_code: code
@@ -163,7 +163,7 @@ Definition return_regs (caller callee: locset) : locset :=
 
 (** Linear execution states. *)
 
-Inductive stackframe: Set :=
+Inductive stackframe: Type :=
   | Stackframe:
       forall (f: function)         (**r calling function *)
              (sp: val)             (**r stack pointer in calling function *)
@@ -171,7 +171,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