diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-01 16:00:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-01 16:00:19 +0000 |
| commit | ef6e39c7df09cb9c48f85bc5a47a82bda9db5383 (patch) | |
| tree | 45a04dbe7b8d8c209b27ffa965df7a2c7bc10604 /ia32 | |
| parent | 5b176de2fb707b4b80fc2b959c8811d3ff0d860a (diff) | |
No longer a dependency on Machtyping
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2132 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Asmgenproof1.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 75d59a4..e3e62cc 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -23,7 +23,6 @@ Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. -Require Import Machtyping. Require Import Asm. Require Import Asmgen. Require Import Asmgenproof0. |