if tl <> [] then
HLog.warn
"Many goals focused. Using the context of the first one\n";
- let _, ctx, _ = NCicUtils.lookup_meta g menv in
- ctx in
+ let ctx = try
+ let _, ctx, _ = NCicUtils.lookup_meta g menv in ctx
+ with NCicUtils.Meta_not_found _ ->
+ HLog.warn "Current goal is closed. Using empty context.";
+ [ ]
+ in ctx
+ in
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
- status None ctx menv subst (parsed_text,parsed_text_length,
+ status `XTNone ctx menv subst (parsed_text,parsed_text_length,
NotationPt.Cast (t,NotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in
let s = NTactics.intros_tac ~names_ref [] script#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
+ [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#status in
try List.assoc "depth" a
with Not_found -> ""
in
- let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " 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
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
+ [s, nl ^ trace ^ thms ^ "/"], "", parsed_text_length
| TA.NAutoInteractive (_, (Some _,_)) -> assert false
let rec eval_executable include_paths (buffer : GText.buffer)