From f811e07f481b135bd7c621c2d10a268dc35d599b Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 17 Apr 2013 10:50:45 +0000 Subject: [PATCH] Fixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a lemma with unskipped goals closed by side-effect. --- matita/components/grafite_engine/grafiteEngine.ml | 3 +++ matita/matita/matitaScript.ml | 9 +++++++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 54850f112..5086eb845 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -663,6 +663,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = | _ -> 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 diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index d86871963..6a03e3538 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -117,8 +117,13 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse 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, -- 2.39.2