diff options
| -rw-r--r-- | arm/CombineOpproof.v | 1 | ||||
| -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 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 1 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 1 | ||||
| -rw-r--r-- | common/Globalenvs.v | 2 | ||||
| -rw-r--r-- | lib/Heaps.v | 1 | ||||
| -rw-r--r-- | lib/Intv.v | 2 | ||||
| -rw-r--r-- | lib/Parmov.v | 2 | ||||
| -rw-r--r-- | powerpc/CombineOpproof.v | 1 | ||||
| -rw-r--r-- | riscV/CombineOpproof.v | 1 | ||||
| -rw-r--r-- | x86/CombineOpproof.v | 1 |
15 files changed, 15 insertions, 3 deletions
diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v index cb30e956..820f4b91 100644 --- a/arm/CombineOpproof.v +++ b/arm/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. 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. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index bea579fc..823d2542 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. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 72b48529..d37fbd46 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -33,7 +33,7 @@ place during program linking and program loading in a real operating system. *) -Require Recdef. +Require Import Recdef. Require Import Zwf. Require Import Axioms Coqlib Errors Maps AST Linking. Require Import Integers Floats Values Memory. 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 2d09171d..db27e83f 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. diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v index 4883876d..cca7606a 100644 --- a/powerpc/CombineOpproof.v +++ b/powerpc/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. 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. diff --git a/x86/CombineOpproof.v b/x86/CombineOpproof.v index a7024501..69abbf61 100644 --- a/x86/CombineOpproof.v +++ b/x86/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 Integers Values Memory. Require Import Op RTL CSEdomain. |