aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r--kernel/cemitcodes.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 3c9692a5c..9ecae2b36 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -10,7 +10,6 @@
machine, Oct 2004 *)
(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
-open Names
open Term
open Cbytecodes
open Copcodes