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 /riscV/CombineOpproof.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 'riscV/CombineOpproof.v')
| -rw-r--r-- | riscV/CombineOpproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/riscV/CombineOpproof.v b/riscV/CombineOpproof.v index 6843da29..a24de1e5 100644 --- a/riscV/CombineOpproof.v +++ b/riscV/CombineOpproof.v @@ -13,6 +13,7 @@ (** Recognition of combined operations, addressing modes and conditions during the [CSE] phase. *) +Require Import FunInd. Require Import Coqlib. Require Import AST. Require Import Integers. |