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 | |
| 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 'lib')
| -rw-r--r-- | lib/Heaps.v | 1 | ||||
| -rw-r--r-- | lib/Intv.v | 2 | ||||
| -rw-r--r-- | lib/Parmov.v | 2 |
3 files changed, 3 insertions, 2 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. @@ -18,7 +18,7 @@ Require Import Coqlib. Require Import Zwf. Require Coq.Program.Wf. -Require Recdef. +Require Import Recdef. Definition interv : Type := (Z * Z)%type. diff --git a/lib/Parmov.v b/lib/Parmov.v index 92bba559..ee7422f4 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -55,7 +55,7 @@ Require Import Relations. Require Import Axioms. Require Import Coqlib. -Require Recdef. +Require Import Recdef. Section PARMOV. |