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

9 files changed, 51 insertions, 49 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 63f0232..91de0b1 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -30,7 +30,7 @@ Require Conventions.
 
 (** Integer registers, floating-point registers. *)
 
-Inductive ireg: Set :=
+Inductive ireg: Type :=
   | GPR0: ireg  | GPR1: ireg  | GPR2: ireg  | GPR3: ireg
   | GPR4: ireg  | GPR5: ireg  | GPR6: ireg  | GPR7: ireg
   | GPR8: ireg  | GPR9: ireg  | GPR10: ireg | GPR11: ireg
@@ -40,7 +40,7 @@ Inductive ireg: Set :=
   | GPR24: ireg | GPR25: ireg | GPR26: ireg | GPR27: ireg
   | GPR28: ireg | GPR29: ireg | GPR30: ireg | GPR31: ireg.
 
-Inductive freg: Set :=
+Inductive freg: Type :=
   | FPR0: freg  | FPR1: freg  | FPR2: freg  | FPR3: freg
   | FPR4: freg  | FPR5: freg  | FPR6: freg  | FPR7: freg
   | FPR8: freg  | FPR9: freg  | FPR10: freg | FPR11: freg
@@ -63,7 +63,7 @@ Proof. decide equality. Defined.
   resolved later by the linker.
 *)
 
-Inductive constant: Set :=
+Inductive constant: Type :=
   | Cint: int -> constant
   | Csymbol_low: ident -> int -> constant
   | Csymbol_high: ident -> int -> constant.
@@ -80,7 +80,7 @@ Inductive constant: Set :=
 (** Bits in the condition register.  We are only interested in the
   first 4 bits. *)
 
-Inductive crbit: Set :=
+Inductive crbit: Type :=
   | CRbit_0: crbit
   | CRbit_1: crbit
   | CRbit_2: crbit
@@ -95,7 +95,7 @@ Inductive crbit: Set :=
 
 Definition label := positive.
 
-Inductive instruction : Set :=
+Inductive instruction : Type :=
   | Padd: ireg -> ireg -> ireg -> instruction                 (**r integer addition *)
   | Paddi: ireg -> ireg -> constant -> instruction            (**r add immediate *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
@@ -303,7 +303,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 *)
   | PC: preg                            (**r program counter *)
@@ -441,7 +441,7 @@ Definition const_high (c: constant) :=
   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.
 
@@ -819,7 +819,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/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 0c3ac75..5c37a57 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -225,7 +225,7 @@ Definition crbit_for_cond (cond: condition) :=
 
 (** Recognition of comparisons [>= 0] and [< 0]. *)
 
-Inductive condition_class: condition -> list mreg -> Set :=
+Inductive condition_class: condition -> list mreg -> Type :=
   | condition_ge0:
       forall n r, n = Int.zero -> condition_class (Ccompimm Cge n) (r :: nil)
   | condition_lt0:
diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v
index 6ec27a3..76ea153 100644
--- a/powerpc/Constprop.v
+++ b/powerpc/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)
@@ -271,7 +271,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)
@@ -696,7 +696,7 @@ Variable approx: D.t.
 Definition intval (r: reg) : option int :=
   match D.get r approx with I n => Some n | _ => None end.
 
-Inductive cond_strength_reduction_cases: condition -> list reg -> Set :=
+Inductive cond_strength_reduction_cases: condition -> list reg -> Type :=
   | csr_case1:
       forall c r1 r2,
       cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil)
@@ -789,7 +789,7 @@ Definition make_xorimm (n: int) (r: reg) :=
   then (Omove, r :: nil)
   else (Oxorimm n, r :: nil).
 
-Inductive op_strength_reduction_cases: operation -> list reg -> Set :=
+Inductive op_strength_reduction_cases: operation -> list reg -> Type :=
   | op_strength_reduction_case1:
       forall (r1: reg) (r2: reg),
       op_strength_reduction_cases Oadd (r1 :: r2 :: nil)
@@ -949,7 +949,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
       (op, args)
   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: reg) (r2: reg),
       addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil)
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index d0f7cf4..88b70c1 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -29,7 +29,7 @@ Require Import AST.
   The type [mreg] does not include special-purpose or reserved
   machine registers such as the stack pointer and the condition codes. *)
 
-Inductive mreg: Set :=
+Inductive mreg: Type :=
   (** Allocatable integer regs *)
   | R3: mreg  | R4: mreg  | R5: mreg  | R6: mreg
   | R7: mreg  | R8: mreg  | R9: mreg  | R10: mreg
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 300a804..27e12c2 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -36,7 +36,7 @@ Set Implicit Arguments.
 
 (** Conditions (boolean-valued operators). *)
 
-Inductive condition : Set :=
+Inductive condition : Type :=
   | Ccomp: comparison -> condition      (**r signed integer comparison *)
   | Ccompu: comparison -> condition     (**r unsigned integer comparison *)
   | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *)
@@ -49,7 +49,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 *)
@@ -104,7 +104,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] *)
   | Aglobal: ident -> int -> addressing (**r Address is [symbol + offset] *)
@@ -182,7 +182,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
@@ -265,7 +265,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 =>
@@ -360,7 +360,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:
@@ -389,14 +389,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.
@@ -497,7 +497,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:
@@ -560,7 +560,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 :=
@@ -746,7 +746,7 @@ End EVAL_OP_TOTAL.
 
 Section EVAL_LESSDEF.
 
-Variable F: Set.
+Variable F: Type.
 Variable genv: Genv.t F.
 
 Ltac InvLessdef :=
@@ -834,7 +834,7 @@ End EVAL_LESSDEF.
 Definition op_for_binary_addressing (addr: addressing) : operation := Oadd.
 
 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/powerpc/Selection.v b/powerpc/Selection.v
index 46d8039..286517e 100644
--- a/powerpc/Selection.v
+++ b/powerpc/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 (t1: expr) (t2: expr),
       notint_cases (Eop Oand (t1:::t2:::Enil))
@@ -208,7 +208,7 @@ Definition addimm (n: int) (e: expr) :=
 
 (** Addition of an integer constant. *)
 
-Inductive addimm_cases: forall (e: expr), Set :=
+Inductive addimm_cases: forall (e: expr), Type :=
   | addimm_case1:
       forall (m: int),
       addimm_cases (Eop (Ointconst m) Enil)
@@ -268,7 +268,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: int) (t2: expr),
       add_cases (Eop (Ointconst n1) Enil) (t2)
@@ -342,7 +342,7 @@ l))
   end.
 *)
 
-Inductive sub_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive sub_cases: forall (e1: expr) (e2: expr), Type :=
   | sub_case1:
       forall (t1: expr) (n2: int),
       sub_cases (t1) (Eop (Ointconst n2) Enil)
@@ -410,7 +410,7 @@ Definition rolm (e1: expr) :=
   end
 *)
 
-Inductive rolm_cases: forall (e1: expr), Set :=
+Inductive rolm_cases: forall (e1: expr), Type :=
   | rolm_case1:
       forall (n1: int),
       rolm_cases (Eop (Ointconst n1) Enil)
@@ -488,7 +488,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)
@@ -532,7 +532,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)
@@ -584,7 +584,7 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
 
 Definition mods := mod_aux Odiv.
 
-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)
@@ -645,7 +645,7 @@ Definition same_expr_pure (e1 e2: expr) :=
   | _, _ => false
   end.
 
-Inductive or_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
   | or_case1:
       forall (amount1: int) (mask1: int) (t1: expr)
              (amount2: int) (mask2: int) (t2: expr),
@@ -678,7 +678,7 @@ Definition or (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)
@@ -723,7 +723,7 @@ Definition addf (e1: expr) (e2: expr) :=
   end.
 *)
 
-Inductive addf_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive addf_cases: forall (e1: expr) (e2: expr), Type :=
   | addf_case1:
       forall (t1: expr) (t2: expr) (t3: expr),
       addf_cases (Eop Omulf (t1:::t2:::Enil)) (t3)
@@ -770,7 +770,7 @@ Definition subf (e1: expr) (e2: expr) :=
   end.
 *)
 
-Inductive subf_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive subf_cases: forall (e1: expr) (e2: expr), Type :=
   | subf_case1:
       forall (t1: expr) (t2: expr) (t3: expr),
       subf_cases (Eop Omulf (t1:::t2:::Enil)) (t3)
@@ -798,7 +798,7 @@ Definition subf (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))
@@ -826,7 +826,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))
@@ -854,7 +854,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))
@@ -882,7 +882,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))
@@ -910,7 +910,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))
@@ -940,7 +940,7 @@ Definition singleoffloat (e: expr) :=
 
 (** ** Comparisons *)
 
-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)
@@ -1043,7 +1043,7 @@ Definition addressing (e: expr) :=
   end.
 *)
 
-Inductive addressing_cases: forall (e: expr), Set :=
+Inductive addressing_cases: forall (e: expr), Type :=
   | addressing_case1:
       forall (s: ident) (n: int),
       addressing_cases (Eop (Oaddrsymbol s n) Enil)
diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v
index 6ffffc1..8a02c99 100644
--- a/powerpc/Selectionproof.v
+++ b/powerpc/Selectionproof.v
@@ -1357,10 +1357,12 @@ 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/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v
index 48e26a7..0de1ccd 100644
--- a/powerpc/eabi/Stacklayout.v
+++ b/powerpc/eabi/Stacklayout.v
@@ -45,7 +45,7 @@ the boundaries between areas in the frame part.
 
 Definition fe_ofs_arg := 8.
 
-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;
diff --git a/powerpc/macosx/Stacklayout.v b/powerpc/macosx/Stacklayout.v
index 0e9be22..c57f3f9 100644
--- a/powerpc/macosx/Stacklayout.v
+++ b/powerpc/macosx/Stacklayout.v
@@ -42,7 +42,7 @@ the boundaries between areas in the frame part.
 
 Definition fe_ofs_arg := 24.
 
-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;