From a834a2aa0dfa9c2da663f5a645a6b086c0321871 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 28 Jun 2010 08:20:04 +0000
Subject: Merging the Princeton implementation of the memory model.  Separate
 axioms in file lib/Axioms.v.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v    | 5 ++++-
 lib/Integers.v  | 3 ++-
 lib/Iteration.v | 1 +
 lib/Parmov.v    | 7 ++++---
 4 files changed, 11 insertions(+), 5 deletions(-)

(limited to 'lib')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 75e158b..4fc922b 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -23,6 +23,8 @@ Require Export List.
 Require Export Bool.
 Require Import Wf_nat.
 
+(***
+
 (** * Logical axioms *)
 
 (** We use two logical axioms that are not provable in Coq but consistent
@@ -36,7 +38,8 @@ Axiom extensionality:
 
 Axiom proof_irrelevance:
   forall (P: Prop) (p1 p2: P), p1 = p2.
-
+***)
+  
 (** * Useful tactics *)
 
 Ltac inv H := inversion H; clear H; subst.
diff --git a/lib/Integers.v b/lib/Integers.v
index f2aca96..f1440e9 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -15,6 +15,7 @@
 
 (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
 
+Require Import Axioms.
 Require Import Coqlib.
 
 (** * Comparisons *)
@@ -115,7 +116,7 @@ Lemma mkint_eq:
   forall x y Px Py, x = y -> mkint x Px = mkint y Py.
 Proof.
   intros. subst y. 
-  generalize (proof_irrelevance _ Px Py); intro.
+  generalize (proof_irr Px Py); intro.
   subst Py. reflexivity.
 Qed.
 
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 24835da..3625845 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -12,6 +12,7 @@
 
 (* Bounded and unbounded iterators *)
 
+Require Import Axioms.
 Require Import Coqlib.
 Require Import Classical.
 Require Import Max.
diff --git a/lib/Parmov.v b/lib/Parmov.v
index edb267e..493b0bd 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -2,8 +2,8 @@
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
-(*      Laurence Rideau, INRIA Sophia-Antipolis-Méditerranée           *)
-(*      Bernard Paul Serpette, INRIA Sophia-Antipolis-Méditerranée     *)
+(*      Laurence Rideau, INRIA Sophia-Antipolis-M\u00e9diterran\u00e9e           *)
+(*      Bernard Paul Serpette, INRIA Sophia-Antipolis-M\u00e9diterran\u00e9e     *)
 (*      Xavier Leroy, INRIA Paris-Rocquencourt                         *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
@@ -53,6 +53,7 @@
 *)
 
 Require Import Relations.
+Require Import Axioms.
 Require Import Coqlib.
 Require Recdef.
 
@@ -99,7 +100,7 @@ Definition env := reg -> val.
 Lemma env_ext:
   forall (e1 e2: env),
   (forall r, e1 r = e2 r) -> e1 = e2.
-Proof (extensionality reg val).
+Proof (@extensionality reg val).
 
 (** The main operation over environments is update: it assigns 
   a value [v] to a register [r] and preserves the values of other
-- 
cgit v1.2.3