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
---
 arm/Op.v | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'arm/Op.v')

diff --git a/arm/Op.v b/arm/Op.v
index bde72520..47cbc0ce 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -34,13 +34,13 @@ Require Import Globalenvs.
 
 Set Implicit Arguments.
 
-Record shift_amount : Set :=
+Record shift_amount : Type :=
   mk_shift_amount { 
     s_amount: int;
     s_amount_ltu: Int.ltu s_amount (Int.repr 32) = true 
   }.
 
-Inductive shift : Set :=
+Inductive shift : Type :=
   | Slsl: shift_amount -> shift
   | Slsr: shift_amount -> shift
   | Sasr: shift_amount -> shift
@@ -48,7 +48,7 @@ Inductive shift : Set :=
 
 (** Conditions (boolean-valued operators). *)
 
-Inductive condition : Set :=
+Inductive condition : Type :=
   | Ccomp: comparison -> condition  (**r signed integer comparison *)
   | Ccompu: comparison -> condition (**r unsigned integer comparison *)
   | Ccompshift: comparison -> shift -> condition  (**r signed integer comparison *)
@@ -61,7 +61,7 @@ Inductive condition : Set :=
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
-Inductive operation : Set :=
+Inductive operation : Type :=
   | Omove: operation                    (**r [rd = r1] *)
   | Ointconst: int -> operation         (**r [rd] is set to the given integer constant *)
   | Ofloatconst: float -> operation     (**r [rd] is set to the given float constant *)
@@ -119,7 +119,7 @@ Inductive operation : Set :=
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the 
   addressing. *)
 
-Inductive addressing: Set :=
+Inductive addressing: Type :=
   | Aindexed: int -> addressing         (**r Address is [r1 + offset] *)
   | Aindexed2: addressing               (**r Address is [r1 + r2] *)
   | Aindexed2shift: shift -> addressing (**r Address is [r1 + shifted r2] *)
@@ -217,7 +217,7 @@ Definition offset_sp (sp: val) (delta: int) : option val :=
   end.
 
 Definition eval_operation
-    (F: Set) (genv: Genv.t F) (sp: val)
+    (F: Type) (genv: Genv.t F) (sp: val)
     (op: operation) (vl: list val): option val :=
   match op, vl with
   | Omove, v1::nil => Some v1
@@ -301,7 +301,7 @@ Definition eval_operation
   end.
 
 Definition eval_addressing
-    (F: Set) (genv: Genv.t F) (sp: val)
+    (F: Type) (genv: Genv.t F) (sp: val)
     (addr: addressing) (vl: list val) : option val :=
   match addr, vl with
   | Aindexed n, Vptr b1 n1 :: nil =>
@@ -382,7 +382,7 @@ Qed.
 
 Section GENV_TRANSF.
 
-Variable F1 F2: Set.
+Variable F1 F2: Type.
 Variable ge1: Genv.t F1.
 Variable ge2: Genv.t F2.
 Hypothesis agree_on_symbols:
@@ -413,14 +413,14 @@ End GENV_TRANSF.
 (** Recognition of move operations. *)
 
 Definition is_move_operation
-    (A: Set) (op: operation) (args: list A) : option A :=
+    (A: Type) (op: operation) (args: list A) : option A :=
   match op, args with
   | Omove, arg :: nil => Some arg
   | _, _ => None
   end.
 
 Lemma is_move_operation_correct:
-  forall (A: Set) (op: operation) (args: list A) (a: A),
+  forall (A: Type) (op: operation) (args: list A) (a: A),
   is_move_operation op args = Some a ->
   op = Omove /\ args = a :: nil.
 Proof.
@@ -523,7 +523,7 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
 
 Section SOUNDNESS.
 
-Variable A: Set.
+Variable A: Type.
 Variable genv: Genv.t A.
 
 Lemma type_of_operation_sound:
@@ -584,7 +584,7 @@ End SOUNDNESS.
 
 Section EVAL_OP_TOTAL.
 
-Variable F: Set.
+Variable F: Type.
 Variable genv: Genv.t F.
 
 Definition find_symbol_offset (id: ident) (ofs: int) : val :=
@@ -774,7 +774,7 @@ End EVAL_OP_TOTAL.
 
 Section EVAL_LESSDEF.
 
-Variable F: Set.
+Variable F: Type.
 Variable genv: Genv.t F.
 
 Ltac InvLessdef :=
@@ -900,7 +900,7 @@ Definition op_for_binary_addressing (addr: addressing) : operation :=
   end.
 
 Lemma eval_op_for_binary_addressing:
-  forall (F: Set) (ge: Genv.t F) sp addr args v,
+  forall (F: Type) (ge: Genv.t F) sp addr args v,
   (length args >= 2)%nat ->
   eval_addressing ge sp addr args = Some v ->
   eval_operation ge sp (op_for_binary_addressing addr) args = Some v.
-- 
cgit