lemma with unskipped goals closed by side-effect.
| _ -> status)
else
status in
| _ -> status)
else
status in
+ (* purge tinycals stack *)
+ let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+ let status = status#set_stack ninitial_stack in
(*
try
index_eq uri status
(*
try
index_eq uri status
if tl <> [] then
HLog.warn
"Many goals focused. Using the context of the first one\n";
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 `XTNone ctx menv subst (parsed_text,parsed_text_length,
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
status `XTNone ctx menv subst (parsed_text,parsed_text_length,