diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-12-30 17:47:53 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-12-30 17:47:53 +0000 |
commit | 5bf13140754a55599ae27942b17cdbb4b7ed74e9 (patch) | |
tree | 57d4ef372149baf47291ad21e65ec77bf9ae15cb /cfrontend | |
parent | 71dfc9f28a1bf4b62c586b3ebee8e2c78088fd84 (diff) |
Remove some useless "Require".
Update ARM port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/ClightBigstep.v | 1 | ||||
-rw-r--r-- | cfrontend/Cminorgen.v | 1 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 1 | ||||
-rw-r--r-- | cfrontend/Cstrategy.v | 1 | ||||
-rw-r--r-- | cfrontend/Csyntax.v | 1 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 1 | ||||
-rw-r--r-- | cfrontend/SimplExpr.v | 2 | ||||
-rw-r--r-- | cfrontend/SimplExprproof.v | 2 | ||||
-rw-r--r-- | cfrontend/SimplExprspec.v | 2 |
9 files changed, 0 insertions, 12 deletions
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 293ea5d..4d10c62 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -16,7 +16,6 @@ (** A big-step semantics for the Clight language. *) Require Import Coqlib. -Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index e024caf..af85971 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -23,7 +23,6 @@ Require Import Ordered. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Memdata. Require Import Csharpminor. Require Import Cminor. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 018fcec..62690d6 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -23,7 +23,6 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Memdata. Require Import Memory. Require Import Events. Require Import Globalenvs. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 0d2f235..b28409d 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -15,7 +15,6 @@ (** A deterministic evaluation strategy for C. *) -Require Import Coq.Program.Equality. Require Import Axioms. Require Import Coqlib. Require Import Errors. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 5155689..6c333aa 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -16,7 +16,6 @@ (** Abstract syntax for the Compcert C language *) Require Import Coqlib. -Require Import Errors. Require Import Integers. Require Import Floats. Require Import Values. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 641ea3c..8757ba2 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -22,7 +22,6 @@ Require Import Memory. Require Import Ctypes. Require Import Cop. Require Import Csyntax. -Require Import Csem. Open Scope error_monad_scope. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 153f177..ab35445 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -22,8 +22,6 @@ Require Import AST. Require Import Ctypes. Require Import Cop. Require Import Csyntax. -Require Import Csem. -Require Cstrategy. Require Import Clight. Module C := Csyntax. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 7fc0a46..59fc9bc 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -12,8 +12,6 @@ (** Correctness proof for expression simplification. *) -Require Import Coq.Program.Equality. -Require Import Axioms. Require Import Coqlib. Require Import Maps. Require Import AST. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 1485dd1..571a937 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -17,13 +17,11 @@ Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. -Require Import Values. Require Import Memory. Require Import AST. Require Import Ctypes. Require Import Cop. Require Import Csyntax. -Require Cstrategy. Require Import Clight. Require Import SimplExpr. |