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, 149 insertions, 148 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index cc5e5ab3..1045d1a0 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -108,7 +108,7 @@ Definition make_globaladdr (id: ident): expr :=
   data block.  [Var_global_scalar] and [Var_global_array] denote
   global variables, stored in the global symbols with the same names. *)
 
-Inductive var_info: Set :=
+Inductive var_info: Type :=
   | Var_local: memory_chunk -> var_info
   | Var_stack_scalar: memory_chunk -> Z -> var_info
   | Var_stack_array: Z -> var_info
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5615eabe..f256bb26 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -225,7 +225,7 @@ Record match_globalenvs (f: meminj) : Prop :=
   collecting information on the current execution state of a Csharpminor
   function and its Cminor translation. *)
 
-Record frame : Set :=
+Record frame : Type :=
   mkframe {
     fr_cenv: compilenv;
     fr_e: Csharpminor.env;
@@ -235,7 +235,7 @@ Record frame : Set :=
     fr_high: Z
   }.
 
-Definition callstack : Set := list frame.
+Definition callstack : Type := list frame.
 
 (** Matching of call stacks imply matching of environments for each of
   the frames, plus matching of the global environments, plus disjointness
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 14b8053d..248192cc 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -426,7 +426,7 @@ Definition empty_env: env := (PTree.empty block).
   how the execution terminated: either normally or prematurely
   through the execution of a [break], [continue] or [return] statement. *)
 
-Inductive outcome: Set :=
+Inductive outcome: Type :=
    | Out_break: outcome                 (**r terminated by [break] *)
    | Out_continue: outcome              (**r terminated by [continue] *)
    | Out_normal: outcome                (**r terminated normally *)
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 1aa536a1..942cfd75 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -37,14 +37,14 @@ Require Import Smallstep.
   be taken using [Eaddrof] expressions.
 *)
 
-Inductive constant : Set :=
+Inductive constant : Type :=
   | Ointconst: int -> constant          (**r integer constant *)
   | Ofloatconst: float -> constant.     (**r floating-point constant *)
 
-Definition unary_operation : Set := Cminor.unary_operation.
-Definition binary_operation : Set := Cminor.binary_operation.
+Definition unary_operation : Type := Cminor.unary_operation.
+Definition binary_operation : Type := Cminor.binary_operation.
 
-Inductive expr : Set :=
+Inductive expr : Type :=
   | Evar : ident -> expr                (**r reading a scalar variable  *)
   | Eaddrof : ident -> expr             (**r taking the address of a variable *)
   | Econst : constant -> expr           (**r constants *)
@@ -59,7 +59,7 @@ Inductive expr : Set :=
   [Sexit n] terminates prematurely the execution of the [n+1] enclosing
   [Sblock] statements. *)
 
-Inductive stmt : Set :=
+Inductive stmt : Type :=
   | Sskip: stmt
   | Sassign : ident -> expr -> stmt
   | Sstore : memory_chunk -> expr -> expr -> stmt
@@ -77,7 +77,7 @@ Inductive stmt : Set :=
   or array variables (of the indicated sizes).  The only operation
   permitted on an array variable is taking its address. *)
 
-Inductive var_kind : Set :=
+Inductive var_kind : Type :=
   | Vscalar: memory_chunk -> var_kind
   | Varray: Z -> var_kind.
 
@@ -86,7 +86,7 @@ Inductive var_kind : Set :=
   local variables with associated [var_kind] description, and a
   statement representing the function body.  *)
 
-Record function : Set := mkfunction {
+Record function : Type := mkfunction {
   fn_sig: signature;
   fn_params: list (ident * memory_chunk);
   fn_vars: list (ident * var_kind);
@@ -95,7 +95,7 @@ Record function : Set := mkfunction {
 
 Definition fundef := AST.fundef function.
 
-Definition program : Set := AST.program fundef var_kind.
+Definition program : Type := AST.program fundef var_kind.
 
 Definition funsig (fd: fundef) :=
   match fd with
@@ -109,7 +109,7 @@ Definition funsig (fd: fundef) :=
   style.  Expressions evaluate to values, and statements evaluate to
   ``outcomes'' indicating how execution should proceed afterwards. *)
 
-Inductive outcome: Set :=
+Inductive outcome: Type :=
   | Out_normal: outcome                (**r continue in sequence *)
   | Out_exit: nat -> outcome           (**r terminate [n+1] enclosing blocks *)
   | Out_return: option val -> outcome. (**r return immediately to caller *)
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 2c010cb4..bd9cf229 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -80,7 +80,7 @@ Qed.
 (** * Properties of the translation functions *)
 
 Lemma map_partial_names:
-  forall (A B: Set) (f: A -> res B)
+  forall (A B: Type) (f: A -> res B)
          (l: list (ident * A)) (tl: list (ident * B)),
   map_partial prefix_var_name f l = OK tl ->
   List.map (@fst ident B) tl = List.map (@fst ident A) l.
@@ -93,7 +93,7 @@ Proof.
 Qed.
    
 Lemma map_partial_append:
-  forall (A B: Set) (f: A -> res B)
+  forall (A B: Type) (f: A -> res B)
          (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)),
   map_partial prefix_var_name f l1 = OK tl1 ->
   map_partial prefix_var_name f l2 = OK tl2 ->
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 75dbc145..af6dc90a 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -865,7 +865,7 @@ Definition eval_funcall_prop
    Csharpminor.eval_funcall tprog m1 tf params t m2 res.
 
 (*
-Set Printing Depth 100.
+Type Printing Depth 100.
 Check (Csem.eval_funcall_ind3 ge exec_stmt_prop exec_lblstmts_prop eval_funcall_prop).
 *)
 
@@ -1592,19 +1592,18 @@ Lemma transl_funcall_divergence_correct:
   Csem.evalinf_funcall ge m1 f params t ->
   wt_fundef (global_typenv prog) f ->
   transl_fundef f = OK tf ->
-  Csharpminor.evalinf_funcall tprog m1 tf params t.
-Proof.
-  cofix FUNCALL.
-  assert (STMT: 
-    forall e m1 s t,
-    Csem.execinf_stmt ge e m1 s t ->
-    forall tyenv nbrk ncnt ts te
-      (WT: wt_stmt tyenv s)
-      (TR: transl_statement nbrk ncnt s = OK ts)   
-      (MENV: match_env tyenv e te),
-    Csharpminor.execinf_stmt tprog te m1 ts t).
-  cofix STMT.
-  assert(LBLSTMT:
+  Csharpminor.evalinf_funcall tprog m1 tf params t
+
+with transl_stmt_divergence_correct:
+  forall e m1 s t,
+  Csem.execinf_stmt ge e m1 s t ->
+  forall tyenv nbrk ncnt ts te
+    (WT: wt_stmt tyenv s)
+    (TR: transl_statement nbrk ncnt s = OK ts)   
+    (MENV: match_env tyenv e te),
+  Csharpminor.execinf_stmt tprog te m1 ts t
+
+with transl_lblstmt_divergence_correct:
   forall s ncnt body ts tyenv e te m0 t0 m1 t1 n,
   transl_lblstmts (lblstmts_length s)
                   (S (lblstmts_length s + ncnt))
@@ -1617,66 +1616,30 @@ Proof.
        /\ execinf_lblstmts ge e m1 (select_switch n s) t1)
    \/ (exec_stmt tprog te m0 body t0 m1 Out_normal
        /\ execinf_lblstmts ge e m1 s t1) ->
-  execinf_stmt_N tprog (lblstmts_length s) te m0 ts (t0 *** t1)).
+  execinf_stmt_N tprog (lblstmts_length s) te m0 ts (t0 *** t1).
 
-  cofix LBLSTMT; intros.
-  destruct s; simpl in *; monadInv H; inv H0.
-  (* 1. LSdefault *)
-  assert (exec_stmt tprog te m0 body t0 m1 Out_normal) by tauto.
-  assert (execinf_lblstmts ge e m1 (LSdefault s) t1) by tauto.
-  clear H2. inv H0.  
-  change (Sblock (Sseq body x))
-    with ((fun z => Sblock z) (Sseq body x)).
-  apply execinf_context. 
-  eapply execinf_Sseq_2. eauto. eapply STMT; eauto. auto.
-  constructor.
-  (* 2. LScase *)
-  elim H2; clear H2.
-  (* 2.1 searching for the case *)
-  rewrite (Int.eq_sym i n). 
-  destruct (Int.eq n i).
-  (* 2.1.1 found it! *)
-  intros [A B]. inv B.
-  (* 2.1.1.1 we diverge because of this case *)
-  destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
-  rewrite EQ1. apply execinf_context; auto. 
-  apply execinf_Sblock. eapply execinf_Sseq_2. eauto. 
-  eapply STMT; eauto. auto.
-  (* 2.1.1.2 we diverge later, after falling through *)
-  simpl. apply execinf_sleep.
-  replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). 
-  eapply LBLSTMT with (n := n); eauto. right. split.
-  change Out_normal with (outcome_block Out_normal). 
-  apply exec_Sblock.
-  eapply exec_Sseq_continue. eauto. 
-  change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
-  eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
-  auto. auto. traceEq.
-  (* 2.1.2 still searching *)
-  rewrite switch_target_table_shift. intros [A B].
-  apply execinf_sleep.
-  eapply LBLSTMT with (n := n); eauto. left. split.
-  fold (outcome_block (Out_exit (switch_target n (lblstmts_length s0) (switch_table s0 0)))).
-  apply exec_Sblock. apply exec_Sseq_stop. eauto. congruence.
-  auto.
-  (* 2.2 found the case already, falling through next cases *)
-  intros [A B]. inv B.
-  (* 2.2.1 we diverge because of this case *)
-  destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
-  rewrite EQ1. apply execinf_context; auto. 
-  apply execinf_Sblock. eapply execinf_Sseq_2. eauto. 
-  eapply STMT; eauto. auto.
-  (* 2.2.2 we diverge later *)
-  simpl. apply execinf_sleep.
-  replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). 
-  eapply LBLSTMT with (n := n); eauto. right. split.
-  change Out_normal with (outcome_block Out_normal). 
-  apply exec_Sblock.
-  eapply exec_Sseq_continue. eauto. 
-  change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
-  eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
-  auto. auto. traceEq.
+Proof.
+  (* Functions *)
+  intros. inv H. 
+  (* Exploitation of typing hypothesis *)
+  inv H0. inv H6. 
+  (* Exploitation of translation hypothesis *)
+  monadInv H1. monadInv EQ.
+  (* Allocation of variables *)
+  assert (match_env (global_typenv prog) Csem.empty_env Csharpminor.empty_env).
+    apply match_globalenv_match_env_empty. apply match_global_typenv. 
+  generalize (transl_fn_variables _ _ (signature_of_function f0) _ _ x2 EQ0 EQ).
+  intro. 
+  destruct (match_env_alloc_variables _ _ _ _ _ _ H2 _ _ _ H1 H5)
+  as [te [ALLOCVARS MATCHENV]].
+  (* Execution *)
+  econstructor; simpl.
+  eapply transl_names_norepet; eauto. 
+  eexact ALLOCVARS.
+  eapply bind_parameters_match; eauto.
+  eapply transl_stmt_divergence_correct; eauto.
 
+(* Statements *)
 
   intros. inv H; inv WT; try (generalize TR; intro TR'; monadInv TR').
   (* Scall *)
@@ -1688,44 +1651,44 @@ Proof.
   eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto.
   eauto. 
   eapply transl_fundef_sig1; eauto. rewrite H3; auto. 
-  eapply FUNCALL; eauto.
+  eapply transl_funcall_divergence_correct; eauto.
   eapply functions_well_typed; eauto.
   (* Sseq 1 *)
-  apply execinf_Sseq_1. eapply STMT; eauto. 
+  apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto. 
   (* Sseq 2 *)
   eapply execinf_Sseq_2. 
   change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
   eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto.
-  eapply STMT; eauto. auto.
+  eapply transl_stmt_divergence_correct; eauto. auto.
   (* Sifthenelse, true *)
   assert (eval_expr tprog te m1 x v1).
     eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
   destruct (make_boolean_correct_true _ _ _ _ _ _ H H1) as [vb [A B]].
   eapply execinf_Sifthenelse. eauto. apply Val.bool_of_true_val; eauto.
-  auto. eapply STMT; eauto.
+  auto. eapply transl_stmt_divergence_correct; eauto.
   (* Sifthenelse, false *)
   assert (eval_expr tprog te m1 x v1).
     eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
   destruct (make_boolean_correct_false _ _ _ _ _ _ H H1) as [vb [A B]].
   eapply execinf_Sifthenelse. eauto. apply Val.bool_of_false_val; eauto.
-  auto. eapply STMT; eauto.
+  auto. eapply transl_stmt_divergence_correct; eauto.
   (* Swhile, body *)
   apply execinf_Sblock. apply execinf_Sloop_body.  
   eapply execinf_Sseq_2. eapply exit_if_false_true; eauto. 
-  apply execinf_Sblock. eapply STMT; eauto. traceEq.
+  apply execinf_Sblock. eapply transl_stmt_divergence_correct; eauto. traceEq.
   (* Swhile, loop *)
   apply execinf_Sblock. eapply execinf_Sloop_block.
   eapply exec_Sseq_continue. eapply exit_if_false_true; eauto.
   rewrite (transl_out_normal_or_continue out1 H3). 
   apply exec_Sblock. 
   eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. reflexivity.
-  eapply STMT with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
+  eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
   constructor; eauto.
   traceEq.
   (* Sdowhile, body *)
   apply execinf_Sblock. apply execinf_Sloop_body.  
   apply execinf_Sseq_1. apply execinf_Sblock.
-  eapply STMT; eauto.
+  eapply transl_stmt_divergence_correct; eauto.
   (* Sdowhile, loop *)
   apply execinf_Sblock. eapply execinf_Sloop_block.
   eapply exec_Sseq_continue.
@@ -1733,21 +1696,21 @@ Proof.
   apply exec_Sblock. 
   eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto. 
   eapply exit_if_false_true; eauto. reflexivity.
-  eapply STMT with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
+  eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
   constructor; auto.
   traceEq.
   (* Sfor start 1 *)
   simpl in TR. destruct (is_Sskip a1). 
   subst a1. inv H0.
   monadInv TR. 
-  apply execinf_Sseq_1. eapply STMT; eauto.
+  apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto.
   (* Sfor start 2 *)
   destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H0) as [ts1 [ts2 [EQ [TR1 TR2]]]].
   subst ts. 
   eapply execinf_Sseq_2. 
   change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
   eapply (transl_stmt_correct _ _ _ _ _ _ H1); eauto.
-  eapply STMT; eauto. 
+  eapply transl_stmt_divergence_correct; eauto. 
     constructor; auto. constructor.
   auto.
   (* Sfor_body *)
@@ -1756,7 +1719,7 @@ Proof.
   eapply execinf_Sseq_2. 
   eapply exit_if_false_true; eauto.
   apply execinf_Sseq_1. apply execinf_Sblock. 
-  eapply STMT; eauto.
+  eapply transl_stmt_divergence_correct; eauto.
   traceEq.
   (* Sfor next *)
   rewrite transl_stmt_Sfor_not_start in TR; monadInv TR.
@@ -1767,7 +1730,7 @@ Proof.
   rewrite (transl_out_normal_or_continue out1 H3). 
   apply exec_Sblock. 
   eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto.
-  eapply STMT; eauto.
+  eapply transl_stmt_divergence_correct; eauto.
   reflexivity. traceEq. 
   (* Sfor loop *)
   generalize TR. rewrite transl_stmt_Sfor_not_start; intro TR'; monadInv TR'.
@@ -1781,7 +1744,7 @@ Proof.
   change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
   eapply (transl_stmt_correct _ _ _ _ _ _ H4); eauto.
   reflexivity. reflexivity. 
-  eapply STMT; eauto. 
+  eapply transl_stmt_divergence_correct; eauto. 
     constructor; auto.
   traceEq.
   (* Sswitch *)
@@ -1790,30 +1753,68 @@ Proof.
   replace (ncnt + lblstmts_length sl + 1)%nat
      with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega.
   change t with (E0 *** t).
-  eapply LBLSTMT; eauto.
+  eapply transl_lblstmt_divergence_correct; eauto.
   left. split. apply exec_Sblock. constructor. 
   eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
-  auto. 
+  auto.
 
-  (* Functions *)
-  intros. inv H. 
-  (* Exploitation of typing hypothesis *)
-  inv H0. inv H6. 
-  (* Exploitation of translation hypothesis *)
-  monadInv H1. monadInv EQ.
-  (* Allocation of variables *)
-  assert (match_env (global_typenv prog) Csem.empty_env Csharpminor.empty_env).
-    apply match_globalenv_match_env_empty. apply match_global_typenv. 
-  generalize (transl_fn_variables _ _ (signature_of_function f0) _ _ x2 EQ0 EQ).
-  intro. 
-  destruct (match_env_alloc_variables _ _ _ _ _ _ H2 _ _ _ H1 H5)
-  as [te [ALLOCVARS MATCHENV]].
-  (* Execution *)
-  econstructor; simpl.
-  eapply transl_names_norepet; eauto. 
-  eexact ALLOCVARS.
-  eapply bind_parameters_match; eauto.
-  eapply STMT; eauto. 
+(* Labeled statements *)
+  intros. destruct s; simpl in *; monadInv H; inv H0.
+  (* 1. LSdefault *)
+  assert (exec_stmt tprog te m0 body t0 m1 Out_normal) by tauto.
+  assert (execinf_lblstmts ge e m1 (LSdefault s) t1) by tauto.
+  clear H2. inv H0.  
+  change (Sblock (Sseq body x))
+    with ((fun z => Sblock z) (Sseq body x)).
+  apply execinf_context. 
+  eapply execinf_Sseq_2. eauto. eapply transl_stmt_divergence_correct; eauto. auto.
+  constructor.
+  (* 2. LScase *)
+  elim H2; clear H2.
+  (* 2.1 searching for the case *)
+  rewrite (Int.eq_sym i n). 
+  destruct (Int.eq n i).
+  (* 2.1.1 found it! *)
+  intros [A B]. inv B.
+  (* 2.1.1.1 we diverge because of this case *)
+  destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
+  rewrite EQ1. apply execinf_context; auto. 
+  apply execinf_Sblock. eapply execinf_Sseq_2. eauto. 
+  eapply transl_stmt_divergence_correct; eauto. auto.
+  (* 2.1.1.2 we diverge later, after falling through *)
+  simpl. apply execinf_sleep.
+  replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). 
+  eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split.
+  change Out_normal with (outcome_block Out_normal). 
+  apply exec_Sblock.
+  eapply exec_Sseq_continue. eauto. 
+  change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
+  eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
+  auto. auto. traceEq.
+  (* 2.1.2 still searching *)
+  rewrite switch_target_table_shift. intros [A B].
+  apply execinf_sleep.
+  eapply transl_lblstmt_divergence_correct with (n := n); eauto. left. split.
+  fold (outcome_block (Out_exit (switch_target n (lblstmts_length s0) (switch_table s0 0)))).
+  apply exec_Sblock. apply exec_Sseq_stop. eauto. congruence.
+  auto.
+  (* 2.2 found the case already, falling through next cases *)
+  intros [A B]. inv B.
+  (* 2.2.1 we diverge because of this case *)
+  destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
+  rewrite EQ1. apply execinf_context; auto. 
+  apply execinf_Sblock. eapply execinf_Sseq_2. eauto. 
+  eapply transl_stmt_divergence_correct; eauto. auto.
+  (* 2.2.2 we diverge later *)
+  simpl. apply execinf_sleep.
+  replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). 
+  eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split.
+  change Out_normal with (outcome_block Out_normal). 
+  apply exec_Sblock.
+  eapply exec_Sseq_continue. eauto. 
+  change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
+  eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
+  auto. auto. traceEq.
 Qed.
 
 End CORRECTNESS.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ac790470..b332e216 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -31,11 +31,11 @@ Require Import AST.
   bit size of the type.  An integer type is a pair of a signed/unsigned
   flag and a bit size: 8, 16 or 32 bits. *)
 
-Inductive signedness : Set :=
+Inductive signedness : Type :=
   | Signed: signedness
   | Unsigned: signedness.
 
-Inductive intsize : Set :=
+Inductive intsize : Type :=
   | I8: intsize
   | I16: intsize
   | I32: intsize.
@@ -43,7 +43,7 @@ Inductive intsize : Set :=
 (** Float types come in two sizes: 32 bits (single precision)
   and 64-bit (double precision). *)
 
-Inductive floatsize : Set :=
+Inductive floatsize : Type :=
   | F32: floatsize
   | F64: floatsize.
 
@@ -82,7 +82,7 @@ Inductive floatsize : Set :=
   structure or union, but not to the structure or union directly.
 *)
 
-Inductive type : Set :=
+Inductive type : Type :=
   | Tvoid: type                            (**r the [void] type *)
   | Tint: intsize -> signedness -> type    (**r integer types *)
   | Tfloat: floatsize -> type              (**r floating-point types *)
@@ -93,11 +93,11 @@ Inductive type : Set :=
   | Tunion: ident -> fieldlist -> type     (**r union types *)
   | Tcomp_ptr: ident -> type               (**r pointer to named struct or union *)
 
-with typelist : Set :=
+with typelist : Type :=
   | Tnil: typelist
   | Tcons: type -> typelist -> typelist
 
-with fieldlist : Set :=
+with fieldlist : Type :=
   | Fnil: fieldlist
   | Fcons: ident -> type -> fieldlist -> fieldlist.
 
@@ -105,12 +105,12 @@ with fieldlist : Set :=
 
 (** Arithmetic and logical operators. *)
 
-Inductive unary_operation : Set :=
+Inductive unary_operation : Type :=
   | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
   | Onotint : unary_operation           (**r integer complement ([~] in C) *)
   | Oneg : unary_operation.             (**r opposite (unary [-]) *)
 
-Inductive binary_operation : Set :=
+Inductive binary_operation : Type :=
   | Oadd : binary_operation             (**r addition (binary [+]) *)
   | Osub : binary_operation             (**r subtraction (binary [-]) *)
   | Omul : binary_operation             (**r multiplication (binary [*]) *)
@@ -138,10 +138,10 @@ Inductive binary_operation : Set :=
   description (type [expr_descr]).
 *)
 
-Inductive expr : Set :=
+Inductive expr : Type :=
   | Expr: expr_descr -> type -> expr
 
-with expr_descr : Set :=
+with expr_descr : Type :=
   | Econst_int: int -> expr_descr       (**r integer literal *)
   | Econst_float: float -> expr_descr   (**r float literal *)
   | Evar: ident -> expr_descr           (**r variable *)
@@ -168,7 +168,7 @@ Definition typeof (e: expr) : type :=
   the [default] case must occur last.  Blocks and block-scoped declarations
   are not supported. *)
 
-Inductive statement : Set :=
+Inductive statement : Type :=
   | Sskip : statement                   (**r do nothing *)
   | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *)
   | Scall: option expr -> expr -> list expr -> statement (**r function call *)
@@ -182,7 +182,7 @@ Inductive statement : Set :=
   | Sreturn : option expr -> statement      (**r [return] statement *)
   | Sswitch : expr -> labeled_statements -> statement  (**r [switch] statement *)
 
-with labeled_statements : Set :=            (**r cases of a [switch] *)
+with labeled_statements : Type :=            (**r cases of a [switch] *)
   | LSdefault: statement -> labeled_statements
   | LScase: int -> statement -> labeled_statements -> labeled_statements.
 
@@ -193,7 +193,7 @@ with labeled_statements : Set :=            (**r cases of a [switch] *)
   and types of its local variables ([fn_vars]), and the body of the
   function (a statement, [fn_body]). *)
 
-Record function : Set := mkfunction {
+Record function : Type := mkfunction {
   fn_return: type;
   fn_params: list (ident * type);
   fn_vars: list (ident * type);
@@ -203,7 +203,7 @@ Record function : Set := mkfunction {
 (** Functions can either be defined ([Internal]) or declared as
   external functions ([External]). *)
 
-Inductive fundef : Set :=
+Inductive fundef : Type :=
   | Internal: function -> fundef
   | External: ident -> typelist -> type -> fundef.
 
@@ -213,7 +213,7 @@ Inductive fundef : Set :=
   of named global variables, carrying their types and optional initialization 
   data.  See module [AST] for more details. *)
 
-Definition program : Set := AST.program fundef type.
+Definition program : Type := AST.program fundef type.
 
 (** * Operations over types *)
 
@@ -409,9 +409,9 @@ Proof.
   destruct (ident_eq id1 i); destruct (ident_eq id2 i).
   congruence. 
   subst i. intros. inv H; inv H0.
-  exploit field_offset_rec_in_range; eauto. tauto. 
+  exploit field_offset_rec_in_range. eexact H1. eauto. tauto.  
   subst i. intros. inv H1; inv H2.
-  exploit field_offset_rec_in_range; eauto. tauto. 
+  exploit field_offset_rec_in_range. eexact H. eauto. tauto. 
   intros. eapply IHfld; eauto.
 
   apply H with fld0 0; auto.
@@ -449,7 +449,7 @@ type must be accessed:
 - [By_nothing]: no access is possible, e.g. for the [void] type.
 *)
 
-Inductive mode: Set :=
+Inductive mode: Type :=
   | By_value: memory_chunk -> mode
   | By_reference: mode
   | By_nothing: mode.
@@ -482,7 +482,7 @@ end.
   compiler (module [Cshmgen]).
 *)
 
-Inductive classify_add_cases : Set :=
+Inductive classify_add_cases : Type :=
   | add_case_ii: classify_add_cases         (**r int , int *)
   | add_case_ff: classify_add_cases         (**r float , float *)
   | add_case_pi: type -> classify_add_cases (**r ptr or array, int *)
@@ -500,7 +500,7 @@ Definition classify_add (ty1: type) (ty2: type) :=
   | _, _ => add_default
   end.
 
-Inductive classify_sub_cases : Set :=
+Inductive classify_sub_cases : Type :=
   | sub_case_ii: classify_sub_cases          (**r int , int *)
   | sub_case_ff: classify_sub_cases          (**r float , float *)
   | sub_case_pi: type -> classify_sub_cases  (**r ptr or array , int *)
@@ -520,7 +520,7 @@ Definition classify_sub (ty1: type) (ty2: type) :=
   | _ ,_ => sub_default
   end.
 
-Inductive classify_mul_cases : Set:=
+Inductive classify_mul_cases : Type:=
   | mul_case_ii: classify_mul_cases (**r int , int *)
   | mul_case_ff: classify_mul_cases (**r float , float *)
   | mul_default: classify_mul_cases . (**r other *)
@@ -532,7 +532,7 @@ Definition classify_mul (ty1: type) (ty2: type) :=
   | _,_  => mul_default
 end.
 
-Inductive classify_div_cases : Set:=
+Inductive classify_div_cases : Type:=
   | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
   | div_case_ii: classify_div_cases    (**r int , int *) 
   | div_case_ff: classify_div_cases    (**r float , float *)
@@ -547,7 +547,7 @@ Definition classify_div (ty1: type) (ty2: type) :=
   | _ ,_ => div_default 
 end.
 
-Inductive classify_mod_cases : Set:=
+Inductive classify_mod_cases : Type:=
   | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
   | mod_case_ii: classify_mod_cases  (**r int , int *)
   | mod_default: classify_mod_cases . (**r other *)
@@ -560,7 +560,7 @@ Definition classify_mod (ty1: type) (ty2: type) :=
   | _ , _ => mod_default 
 end .
 
-Inductive classify_shr_cases :Set:=
+Inductive classify_shr_cases :Type:=
   | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
   | shr_case_ii :classify_shr_cases (**r int , int *)
   | shr_default : classify_shr_cases . (**r other *)
@@ -572,7 +572,7 @@ Definition classify_shr (ty1: type) (ty2: type) :=
   | _ , _ => shr_default 
   end.
 
-Inductive classify_cmp_cases : Set:=
+Inductive classify_cmp_cases : Type:=
   | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
   | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
   | cmp_case_ff: classify_cmp_cases  (**r float , float *)
@@ -593,7 +593,7 @@ Definition classify_cmp (ty1: type) (ty2: type) :=
   | _ , _ => cmp_default
   end.
 
-Inductive classify_fun_cases : Set:=
+Inductive classify_fun_cases : Type:=
   | fun_case_f: typelist -> type -> classify_fun_cases   (**r (pointer to) function *)
   | fun_default: classify_fun_cases . (**r other *)