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
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