From 04f6ca789cac88220234a3bdfb497844c417ef14 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2011 12:06:38 +0000 Subject: [PATCH] intros macro fixed --- matita/matita/matitaScript.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 6bf9e5e02..bf8da8eb4 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -132,7 +132,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse 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 -- 2.39.2