aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v5
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.