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 /backend/ValueDomain.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 'backend/ValueDomain.v')
-rw-r--r-- | backend/ValueDomain.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index f905ffa2..c71b515c 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +Require Import FunInd. Require Import Zwf Coqlib Maps Integers Floats Lattice. Require Import Compopts AST. Require Import Values Memory Globalenvs Events. |