Merge branch 'master' into add-file

5 files changed, 33 insertions, 34 deletions

diff --git a/common/AST.v b/common/AST.v
index 0b524eb8..ae7178f4 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -684,7 +684,7 @@ Inductive builtin_arg_constraint : Type :=
 Definition builtin_arg_ok
        (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
   match ba, c with
-  | (BA _ | BA_splitlong _ _), _ => true
+  | (BA _ | BA_splitlong (BA _) (BA _)), _ => true
   | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true
   | BA_addrstack _, (OK_addrstack | OK_addrany) => true
   | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true
diff --git a/common/Memory.v b/common/Memory.v
index f32d21c7..672012be 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1500,11 +1500,11 @@ Qed.
 Theorem loadbytes_storebytes_same:
   loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
 Proof.
-  intros. unfold storebytes in STORE. unfold loadbytes.
+  intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. 
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
   try discriminate.
   rewrite pred_dec_true.
-  decEq. inv STORE; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat.
+  decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat.
   apply getN_setN_same.
   red; eauto with mem.
 Qed.
diff --git a/common/Separation.v b/common/Separation.v
index 6a7ffbea..efcd3281 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -620,7 +620,7 @@ Next Obligation.
     eauto with mem. }
   destruct H. constructor.
 - destruct mi_inj. constructor; intros.
-+ eapply Mem.perm_unchanged_on; eauto. eapply IMG; eauto.
++ eapply Mem.perm_unchanged_on; eauto.
 + eauto.
 + rewrite (Mem.unchanged_on_contents _ _ _ H0); eauto.
 - assumption.
@@ -630,7 +630,6 @@ Next Obligation.
 - intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto.
   eapply mi_perm_inv; eauto. 
   eapply Mem.perm_unchanged_on_2; eauto.
-  eapply IMG; eauto. 
 Qed.
 Next Obligation.
   eapply Mem.valid_block_inject_2; eauto.
diff --git a/common/Subtyping.v b/common/Subtyping.v
index c09226e0..26b282e0 100644
--- a/common/Subtyping.v
+++ b/common/Subtyping.v
@@ -30,48 +30,48 @@ Module Type TYPE_ALGEBRA.
 
 (** Type expressions *)
 
-Variable t: Type.
-Variable eq: forall (x y: t), {x=y} + {x<>y}.
-Variable default: t.
+Parameter t: Type.
+Parameter eq: forall (x y: t), {x=y} + {x<>y}.
+Parameter default: t.
 
 (** Subtyping *)
 
-Variable sub: t -> t -> Prop.
-Hypothesis sub_refl: forall x, sub x x.
-Hypothesis sub_trans: forall x y z, sub x y -> sub y z -> sub x z.
-Variable sub_dec: forall x y, {sub x y} + {~sub x y}.
+Parameter sub: t -> t -> Prop.
+Axiom sub_refl: forall x, sub x x.
+Axiom sub_trans: forall x y z, sub x y -> sub y z -> sub x z.
+Parameter sub_dec: forall x y, {sub x y} + {~sub x y}.
 
 (** Least upper bounds. [lub x y] is specified only when [x] and [y] have
   a common supertype; it can be arbitrary otherwise. *)
 
-Variable lub: t -> t -> t.
-Hypothesis lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y).
-Hypothesis lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y).
-Hypothesis lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z.
+Parameter lub: t -> t -> t.
+Axiom lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y).
+Axiom lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y).
+Axiom lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z.
 
 (** Greater lower bounds. [glb x y] is specified only when [x] and [y] have
   a common subtype; it can be arbitrary otherwise.*)
 
-Variable glb: t -> t -> t.
-Hypothesis glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x.
-Hypothesis glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y.
-Hypothesis glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y).
+Parameter glb: t -> t -> t.
+Axiom glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x.
+Axiom glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y.
+Axiom glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y).
 
 (** Low and high bounds for a given type. *)
-Variable low_bound: t -> t.
-Variable high_bound: t -> t.
-Hypothesis low_bound_sub: forall t, sub (low_bound t) t.
-Hypothesis low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x.
-Hypothesis high_bound_sub: forall t, sub t (high_bound t).
-Hypothesis high_bound_majorant: forall x y, sub x y -> sub y (high_bound x).
+Parameter low_bound: t -> t.
+Parameter high_bound: t -> t.
+Axiom low_bound_sub: forall t, sub (low_bound t) t.
+Axiom low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x.
+Axiom high_bound_sub: forall t, sub t (high_bound t).
+Axiom high_bound_majorant: forall x y, sub x y -> sub y (high_bound x).
 
 (** Measure over types *)
 
-Variable weight: t -> nat.
-Variable max_weight: nat.
-Hypothesis weight_range: forall t, weight t <= max_weight.
-Hypothesis weight_sub: forall x y, sub x y -> weight x <= weight y.
-Hypothesis weight_sub_strict: forall x y, sub x y -> x <> y -> weight x < weight y.
+Parameter weight: t -> nat.
+Parameter max_weight: nat.
+Axiom weight_range: forall t, weight t <= max_weight.
+Axiom weight_sub: forall x y, sub x y -> weight x <= weight y.
+Axiom weight_sub_strict: forall x y, sub x y -> x <> y -> weight x < weight y.
 
 End TYPE_ALGEBRA.
 
diff --git a/common/Unityping.v b/common/Unityping.v
index f9c9d72c..28bcfb5c 100644
--- a/common/Unityping.v
+++ b/common/Unityping.v
@@ -28,9 +28,9 @@ Local Open Scope error_monad_scope.
 
 Module Type TYPE_ALGEBRA.
 
-Variable t: Type.
-Variable eq: forall (x y: t), {x=y} + {x<>y}.
-Variable default: t.
+Parameter t: Type.
+Parameter eq: forall (x y: t), {x=y} + {x<>y}.
+Parameter default: t.
 
 End TYPE_ALGEBRA.