aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/discharge.ml')
-rw-r--r--toplevel/discharge.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 11ed968a9..b1ba1f748 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -17,7 +17,6 @@ open Term
open Declarations
open Entries
open Inductive
-open Instantiate
open Reduction
open Cooking
open Typeops