aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index e6d7613b00..7751e5bf6e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -16,7 +16,6 @@ open Sign
open Declarations
open Environ
open Reduction
-open Term_typing
(*s Cooking the constants. *)