diff options
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 2 |
1 files changed, 0 insertions, 2 deletions
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. |