+ | TA.NIntroGuess _loc ->
+ let names_ref = ref [] in
+ let s =
+ NTactics.intros_tac ~names_ref [] script#grafite_status
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length