diff options
| author | Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> | 2017-07-20 11:10:00 +0200 |
|---|---|---|
| committer | Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> | 2017-07-20 11:20:52 +0200 |
| commit | b26b8d219230ae912e3860dc906d34169af2a5c8 (patch) | |
| tree | acb660fe64b791e5999a24cf844cc83567c68557 /common/Globalenvs.v | |
| parent | 2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6 (diff) | |
| download | compcert-kvx-b26b8d219230ae912e3860dc906d34169af2a5c8.tar.gz compcert-kvx-b26b8d219230ae912e3860dc906d34169af2a5c8.zip | |
Ensure FunInd or Recdef is imported if functional induction is used
Coq 8.7 does not load FunInd in prelude anymore, so this is necessary.
Recdef exports FunInd, so if Recdef is imported, importing FunInd
is not required.
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. |