]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaScript.ml
removed dead code (thanks to ocaml 3.09)
[helm.git] / helm / matita / matitaScript.ml
index 3fa4e93e7bf71ed7c68a74f306fc7f74f4daba4e..08e3a45991ce6a53fbd9dbc5d2916e2245d6aa30 100644 (file)
@@ -230,7 +230,6 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   let module CTC = CicTypeChecker in
   let module CU = CicUniv in
   (* no idea why ocaml wants this *)
-  let advance ?statement () = script#advance ?statement () in
   let parsed_text_length = String.length parsed_text in
   let dbd = MatitaDb.instance () in
   match mac with
@@ -347,7 +346,6 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
   let module TAPp = GrafiteAstPp in
   let module MD = MatitaDisambiguator in
   let module ML = MatitacleanLib in
-  let parsed_text_length = String.length parsed_text in
   match ex with
   | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
       (try