From 341c09ae53c5b432015dbd95ac099d824609e626 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jul 2009 12:46:08 +0000 Subject: [PATCH] Useless "let module" removed. --- helm/software/matita/matitaScript.ml | 8 -------- 1 file changed, 8 deletions(-) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index e72644d10..2055bb9cd 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -74,8 +74,6 @@ type guistuff = { let eval_with_engine include_paths guistuff grafite_status user_goal skipped_txt nonskipped_txt st = - let module TAPp = GrafiteAstPp in - let module DTE = DisambiguateTypes.Environment in let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt in @@ -369,11 +367,8 @@ let cic2grafite context menv t = ;; let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = - let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in - let module MDB = LibraryDb in let module CTC = CicTypeChecker in - let module CU = CicUniv in (* no idea why ocaml wants this *) let parsed_text_length = String.length parsed_text in let dbd = LibraryDb.instance () in @@ -581,9 +576,6 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = - let module TAPp = GrafiteAstPp in - let module MD = MultiPassDisambiguator in - let module ML = MatitaMisc in try ignore (buffer#move_mark (`NAME "beginning_of_statement") ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars -- 2.39.2