From 667640d70feb01f2a800b548fa019c92b103d75a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 Oct 2009 13:35:24 +0000 Subject: [PATCH] ncheck is not erased --- helm/software/matita/matitaScript.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index a67075a29..829806871 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -392,7 +392,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us (* XXX use the metasenv, if possible *) in guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); - [], "", parsed_text_length + [status, parsed_text], "", parsed_text_length let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = let module MQ = MetadataQuery in -- 2.39.2