diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-10-20 10:34:31 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-20 10:34:31 +0200 |
| commit | b4f59c4773206fbdf850611e6bbac1767d459dd5 (patch) | |
| tree | 407ae2638eeca041e843c2fbbbaa75fd595df02e /backend | |
| parent | 6a010b47b216c5a6b6e85abcfbba5339bab15dd6 (diff) | |
| parent | b26b8d219230ae912e3860dc906d34169af2a5c8 (diff) | |
| download | compcert-b4f59c4773206fbdf850611e6bbac1767d459dd5.tar.gz compcert-b4f59c4773206fbdf850611e6bbac1767d459dd5.zip | |
Merge pull request #191 from sigurdschneider/master
Ensure FunInd or Recdef is imported if functional induction is used.
This is necessary for Coq 8.7.0.
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocproof.v | 1 | ||||
| -rw-r--r-- | backend/Deadcodeproof.v | 1 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 1 | ||||
| -rw-r--r-- | backend/ValueAnalysis.v | 1 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 1 |
5 files changed, 5 insertions, 0 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 4b75e34d..585fb0da 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -13,6 +13,7 @@ (** Correctness proof for the [Allocation] pass (validated translation from RTL to LTL). *) +Require Import FunInd. Require Import FSets. Require Import Coqlib Ordered Maps Errors Integers Floats. Require Import AST Linking Lattice Kildall. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 12c05cc3..199ac922 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -12,6 +12,7 @@ (** Elimination of unneeded computations over RTL: correctness proof. *) +Require Import FunInd. Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Values Memory Globalenvs Events Smallstep. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 86d7ff21..dc01ad20 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -12,6 +12,7 @@ (** Correctness of instruction selection *) +Require Import FunInd. Require Import Coqlib Maps. Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep. Require Import Switch Cminor Op CminorSel. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 674bc065..3c3aecfd 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +Require Import FunInd. Require Import Coqlib Maps Integers Floats Lattice Kildall. Require Import Compopts AST Linking. Require Import Values Memory Globalenvs Events. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index d7eaa228..7cf947ba 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. |