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 /lib/Heaps.v | |
parent | 2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6 (diff) | |
download | compcert-b26b8d219230ae912e3860dc906d34169af2a5c8.tar.gz compcert-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 'lib/Heaps.v')
-rw-r--r-- | lib/Heaps.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/Heaps.v b/lib/Heaps.v index 65334a38..2a21f88c 100644 --- a/lib/Heaps.v +++ b/lib/Heaps.v @@ -21,6 +21,7 @@ (If an element is already in a heap, inserting it again does nothing.) *) +Require Import FunInd. Require Import Coqlib. Require Import FSets. Require Import Ordered. |