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/Integers.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'lib/Integers.v')

diff --git a/lib/Integers.v b/lib/Integers.v
index f2aca962..f1440e9e 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.
 
-- 
cgit