diff options
Diffstat (limited to 'common/Globalenvs.v')
| -rw-r--r-- | common/Globalenvs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index dd8a1eb9..25830477 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -33,7 +33,7 @@ place during program linking and program loading in a real operating system. *) -Require Recdef. +Require Import Recdef. Require Import Zwf. Require Import Axioms Coqlib Errors Maps AST Linking. Require Import Integers Floats Values Memory. |