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
---
 common/Globalenvs.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'common/Globalenvs.v')

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index b540ad12..a29c2496 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -33,6 +33,7 @@
   place during program linking and program loading in a real operating
   system. *)
 
+Require Import Axioms.
 Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
-- 
cgit