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 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 75e158bd..4fc922b1 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.
-- 
cgit