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 /cfrontend | |
| 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 'cfrontend')
| -rw-r--r-- | cfrontend/Cexec.v | 1 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index a9ffcd3d..e063dfc3 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -12,6 +12,7 @@ (** Animating the CompCert C semantics *) +Require Import FunInd. Require Import Axioms Classical. Require Import String Coqlib Decidableplus. Require Import Errors Maps Integers Floats. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index d85fb271..ee1df409 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -12,6 +12,7 @@ (** Correctness proof for expression simplification. *) +Require Import FunInd. Require Import Coqlib Maps Errors Integers. Require Import AST Linking. Require Import Values Memory Events Globalenvs Smallstep. |