- cic_exportation, cic_acic, acic_content (only parts related to acic)

[helm.git] / matita / matita / matitaScript.ml

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index b6ec2a51f01262a58b483a093a7dafea26b4f7c1..62305ec00add30449f14bdbe49728ce1761a90d6 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -191,7 +191,6 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
   | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
-  let module CTC = CicTypeChecker in
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in