- | 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
- | TA.NAutoInteractive (_loc, (None,a)) ->
- let trace_ref = ref [] in
- let s =
- NnAuto.auto_tac
- ~params:(None,a) ~trace_ref script#grafite_status
- in
- let depth =
- try List.assoc "depth" a
- with Not_found -> ""
- in
- let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
- let thms =
- match !trace_ref with
- | [] -> "{}"
- | thms ->
- String.concat ", "
- (HExtlib.filter_map (function
- | CicNotationPt.NRef r -> Some (NCicPp.r2s true r)
- | _ -> None)
- thms)
- 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 ^ trace ^ thms ^ ";"], "", parsed_text_length
- | TA.NAutoInteractive (_, (Some _,_)) -> assert false