diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
| commit | 4c379d48b35e7c8156f3953fede31d5e47faf8ca (patch) | |
| tree | fa19eb30178fcf74b0768d9f5df4017ab6afc770 /extraction | |
| parent | 3b79923a6c9fa8c76916df1eecfdecd7ae2124a5 (diff) | |
| download | compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.tar.gz compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.zip | |
helpers broke compilation
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 5a1ca0be..caf4330b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,11 +34,6 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. -<<<<<<< HEAD -Require Int31. -Require Asmaux. -======= ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf (* Standard lib *) Require Import ExtrOcamlBasic. |