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

7 files changed, 52 insertions, 56 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 3bb2cca2..79feee72 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -30,13 +30,13 @@ Require Conventions.
 
 (** Integer registers, floating-point registers. *)
 
-Inductive ireg: Set :=
+Inductive ireg: Type :=
   | IR0: ireg  | IR1: ireg  | IR2: ireg  | IR3: ireg
   | IR4: ireg  | IR5: ireg  | IR6: ireg  | IR7: ireg
   | IR8: ireg  | IR9: ireg  | IR10: ireg | IR11: ireg
   | IR12: ireg | IR13: ireg | IR14: ireg.
 
-Inductive freg: Set :=
+Inductive freg: Type :=
   | FR0: freg  | FR1: freg  | FR2: freg  | FR3: freg
   | FR4: freg  | FR5: freg  | FR6: freg  | FR7: freg.
 
@@ -48,7 +48,7 @@ Proof. decide equality. Defined.
 
 (** Bits in the condition register. *)
 
-Inductive crbit: Set :=
+Inductive crbit: Type :=
   | CReq: crbit    (**r equal *)
   | CRne: crbit    (**r not equal *)
   | CRhs: crbit    (**r unsigned higher or same *)
@@ -74,7 +74,7 @@ Proof. decide equality. Defined.
 
 Definition label := positive.
 
-Inductive shift_op : Set :=
+Inductive shift_op : Type :=
   | SOimm: int -> shift_op
   | SOreg: ireg -> shift_op
   | SOlslimm: ireg -> int -> shift_op
@@ -86,7 +86,7 @@ Inductive shift_op : Set :=
   | SOrorimm: ireg -> int -> shift_op
   | SOrorreg: ireg -> ireg -> shift_op.
 
-Inductive shift_addr : Set :=
+Inductive shift_addr : Type :=
   | SAimm: int -> shift_addr
   | SAreg: ireg -> shift_addr
   | SAlsl: ireg -> int -> shift_addr
@@ -94,7 +94,7 @@ Inductive shift_addr : Set :=
   | SAasr: ireg -> int -> shift_addr
   | SAror: ireg -> int -> shift_addr.
 
-Inductive instruction : Set :=
+Inductive instruction : Type :=
   (* Core instructions *)
   | Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *)
   | Pand: ireg -> ireg -> shift_op -> instruction (**r bitwise and *)
@@ -242,7 +242,7 @@ Definition program := AST.program fundef unit.
 (** The PowerPC has a great many registers, some general-purpose, some very
   specific.  We model only the following registers: *)
 
-Inductive preg: Set :=
+Inductive preg: Type :=
   | IR: ireg -> preg                    (**r integer registers *)
   | FR: freg -> preg                    (**r float registers *)
   | CR: crbit -> preg                   (**r bits in the condition register *)
@@ -315,7 +315,7 @@ Variable ge: genv.
   set and memory state after execution of the instruction at [rs#PC],
   or [Error] if the processor is stuck. *)
 
-Inductive outcome: Set :=
+Inductive outcome: Type :=
   | OK: regset -> mem -> outcome
   | Error: outcome.
 
@@ -621,7 +621,7 @@ Definition loc_external_result (sg: signature) : preg :=
 
 (** Execution of the instruction at [rs#PC]. *)
 
-Inductive state: Set :=
+Inductive state: Type :=
   | State: regset -> mem -> state.
 
 Inductive step: state -> trace -> state -> Prop :=
diff --git a/arm/Constprop.v b/arm/Constprop.v
index b51d974e..5bd84b6d 100644
--- a/arm/Constprop.v
+++ b/arm/Constprop.v
@@ -32,7 +32,7 @@ Require Import Kildall.
 (** To each pseudo-register at each program point, the static analysis 
   associates a compile-time approximation taken from the following set. *)
 
-Inductive approx : Set :=
+Inductive approx : Type :=
   | Novalue: approx      (** No value possible, code is unreachable. *)
   | Unknown: approx      (** All values are possible,
                              no compile-time information is available. *)
@@ -139,7 +139,7 @@ Definition eval_static_condition (cond: condition) (vl: list approx) :=
   end.
 *)
 
-Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Set :=
+Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type :=
   | eval_static_condition_case1:
       forall c n1 n2,
       eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil)
@@ -274,7 +274,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   end.
 *)
 
-Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Set :=
+Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type :=
   | eval_static_operation_case1:
       forall v1,
       eval_static_operation_cases (Omove) (v1::nil)
@@ -735,7 +735,7 @@ Definition cond_strength_reduction (cond: condition) (args: list reg) :=
   end.
 *)
 
-Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg), Set :=
+Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg), Type :=
   | cond_strength_reduction_case1:
       forall c r1 r2,
       cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil)
@@ -886,7 +886,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
   end.
 *)
 
-Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg), Set :=
+Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg), Type :=
   | op_strength_reduction_case1:
       forall r1 r2,
       op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil)
@@ -1120,7 +1120,7 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) :=
   end.
 *)
 
-Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Set :=
+Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Type :=
   | addr_strength_reduction_case1:
       forall r1 r2,
       addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil)
diff --git a/arm/Machregs.v b/arm/Machregs.v
index 3466c0b0..2e422d27 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -29,7 +29,7 @@ Require Import AST.
   The type [mreg] does not include special-purpose machine registers
   such as the stack pointer and the condition codes. *)
 
-Inductive mreg: Set :=
+Inductive mreg: Type :=
   (** Allocatable integer regs *)
   | R0: mreg  | R1: mreg  | R2: mreg  | R3: mreg
   | R4: mreg  | R5: mreg  | R6: mreg  | R7: mreg
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.
diff --git a/arm/Selection.v b/arm/Selection.v
index d04a4ca3..12cc1b27 100644
--- a/arm/Selection.v
+++ b/arm/Selection.v
@@ -118,7 +118,7 @@ Definition notint (e: expr) :=
   characterizes the expressions that match each of the 4 cases of interest.
 *)
 
-Inductive notint_cases: forall (e: expr), Set :=
+Inductive notint_cases: forall (e: expr), Type :=
   | notint_case1:
       forall s t1,
       notint_cases (Eop (Oshift s) (t1:::Enil))
@@ -208,7 +208,7 @@ Definition addimm (n: int) (e: expr) :=
   end.
 *)
 
-Inductive addimm_cases: forall (e: expr), Set :=
+Inductive addimm_cases: forall (e: expr), Type :=
   | addimm_case1:
       forall m,
       addimm_cases (Eop (Ointconst m) Enil)
@@ -270,7 +270,7 @@ Definition add (e1: expr) (e2: expr) :=
   end.
 *)
 
-Inductive add_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
   | add_case1:
       forall n1 t2,
       add_cases (Eop (Ointconst n1) Enil) (t2)
@@ -352,7 +352,7 @@ Definition sub (e1: expr) (e2: expr) :=
   end.
 *)
 
-Inductive sub_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive sub_cases: forall (e1: expr) (e2: expr), Type :=
   | sub_case1:
       forall t1 n2,
       sub_cases (t1) (Eop (Ointconst n2) Enil)
@@ -430,7 +430,7 @@ Definition shlimm (e1: expr) :=
   end.
 *)
 
-Inductive shlimm_cases: forall (e1: expr), Set :=
+Inductive shlimm_cases: forall (e1: expr), Type :=
   | shlimm_case1:
       forall n1,
       shlimm_cases (Eop (Ointconst n1) Enil)
@@ -481,7 +481,7 @@ Definition shruimm (e1: expr) :=
   end.
 *)
 
-Inductive shruimm_cases: forall (e1: expr), Set :=
+Inductive shruimm_cases: forall (e1: expr), Type :=
   | shruimm_case1:
       forall n1,
       shruimm_cases (Eop (Ointconst n1) Enil)
@@ -531,7 +531,7 @@ Definition shrimm (e1: expr) :=
   end.
 *)
 
-Inductive shrimm_cases: forall (e1: expr), Set :=
+Inductive shrimm_cases: forall (e1: expr), Type :=
   | shrimm_case1:
       forall n1,
       shrimm_cases (Eop (Ointconst n1) Enil)
@@ -598,7 +598,7 @@ Definition mulimm (n1: int) (e2: expr) :=
   end.
 *)
 
-Inductive mulimm_cases: forall (e2: expr), Set :=
+Inductive mulimm_cases: forall (e2: expr), Type :=
   | mulimm_case1:
       forall (n2: int),
       mulimm_cases (Eop (Ointconst n2) Enil)
@@ -642,7 +642,7 @@ Definition mul (e1: expr) (e2: expr) :=
   end.
 *)
 
-Inductive mul_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive mul_cases: forall (e1: expr) (e2: expr), Type :=
   | mul_case1:
       forall (n1: int) (t2: expr),
       mul_cases (Eop (Ointconst n1) Enil) (t2)
@@ -690,7 +690,7 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
                            Enil) :::
                  Enil))).
 
-Inductive divu_cases: forall (e2: expr), Set :=
+Inductive divu_cases: forall (e2: expr), Type :=
   | divu_case1:
       forall (n2: int),
       divu_cases (Eop (Ointconst n2) Enil)
@@ -759,7 +759,7 @@ Definition and (e1: expr) (e2: expr) :=
   end.
 *)
 
-Inductive and_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive and_cases: forall (e1: expr) (e2: expr), Type :=
   | and_case1:
       forall s t1 t2,
       and_cases (Eop (Oshift s) (t1:::Enil)) (t2)
@@ -836,7 +836,7 @@ Definition or (e1: expr) (e2: expr) :=
 
 (* TODO: symmetric of first case *)
 
-Inductive or_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
   | or_case1:
       forall n1 t1 n2 t2,
       or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil))
@@ -886,7 +886,7 @@ Definition xor (e1: expr) (e2: expr) :=
   end.
 *)
 
-Inductive xor_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive xor_cases: forall (e1: expr) (e2: expr), Type :=
   | xor_case1:
       forall s t1 t2,
       xor_cases (Eop (Oshift s) (t1:::Enil)) (t2)
@@ -919,7 +919,7 @@ Definition xor (e1: expr) (e2: expr) :=
 
 (** ** General shifts *)
 
-Inductive shift_cases: forall (e1: expr), Set :=
+Inductive shift_cases: forall (e1: expr), Type :=
   | shift_case1:
       forall (n2: int),
       shift_cases (Eop (Ointconst n2) Enil)
@@ -961,7 +961,7 @@ Definition shr (e1: expr) (e2: expr) :=
 
 (** ** Truncations and sign extensions *)
 
-Inductive cast8signed_cases: forall (e1: expr), Set :=
+Inductive cast8signed_cases: forall (e1: expr), Type :=
   | cast8signed_case1:
       forall (e2: expr),
       cast8signed_cases (Eop Ocast8signed (e2 ::: Enil))
@@ -983,7 +983,7 @@ Definition cast8signed (e: expr) :=
   | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil)
   end.
 
-Inductive cast8unsigned_cases: forall (e1: expr), Set :=
+Inductive cast8unsigned_cases: forall (e1: expr), Type :=
   | cast8unsigned_case1:
       forall (e2: expr),
       cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil))
@@ -1005,7 +1005,7 @@ Definition cast8unsigned (e: expr) :=
   | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil)
   end.
 
-Inductive cast16signed_cases: forall (e1: expr), Set :=
+Inductive cast16signed_cases: forall (e1: expr), Type :=
   | cast16signed_case1:
       forall (e2: expr),
       cast16signed_cases (Eop Ocast16signed (e2 ::: Enil))
@@ -1027,7 +1027,7 @@ Definition cast16signed (e: expr) :=
   | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil)
   end.
 
-Inductive cast16unsigned_cases: forall (e1: expr), Set :=
+Inductive cast16unsigned_cases: forall (e1: expr), Type :=
   | cast16unsigned_case1:
       forall (e2: expr),
       cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil))
@@ -1049,7 +1049,7 @@ Definition cast16unsigned (e: expr) :=
   | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil)
   end.
 
-Inductive singleoffloat_cases: forall (e1: expr), Set :=
+Inductive singleoffloat_cases: forall (e1: expr), Type :=
   | singleoffloat_case1:
       forall (e2: expr),
       singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil))
@@ -1084,7 +1084,7 @@ Definition comp (e1: expr) (e2: expr) :=
   end.
 *)
   
-Inductive comp_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive comp_cases: forall (e1: expr) (e2: expr), Type :=
   | comp_case1:
       forall n1 t2,
       comp_cases (Eop (Ointconst n1) Enil) (t2)
@@ -1204,7 +1204,7 @@ Definition addressing (e: expr) :=
   end.
 *)
 
-Inductive addressing_cases: forall (e: expr), Set :=
+Inductive addressing_cases: forall (e: expr), Type :=
   | addressing_case2:
       forall n,
       addressing_cases (Eop (Oaddrstack n) Enil)
diff --git a/arm/Selectionproof.v b/arm/Selectionproof.v
index 10f93f3a..967e2292 100644
--- a/arm/Selectionproof.v
+++ b/arm/Selectionproof.v
@@ -1389,10 +1389,6 @@ Proof.
   econstructor. destruct k; simpl in H; simpl; auto. 
   rewrite <- H0; reflexivity.
   constructor; auto.
-  (* assign *)
-  exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split.
-  constructor. auto with evalexpr.
-  constructor; auto.
   (* store *)
   econstructor; split.
   eapply eval_store; eauto with evalexpr.
diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v
index dd3c6a1d..b374bfd9 100644
--- a/arm/linux/Stacklayout.v
+++ b/arm/linux/Stacklayout.v
@@ -40,7 +40,7 @@ the boundaries between areas in the frame part.
 
 Definition fe_ofs_arg := 0.
 
-Record frame_env : Set := mk_frame_env {
+Record frame_env : Type := mk_frame_env {
   fe_size: Z;
   fe_ofs_link: Z;
   fe_ofs_retaddr: Z;