From daad2a4dda4e4b0eed3c1cd57846a31da5f706a5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 11 Jan 2011 21:29:25 +0000 Subject: [PATCH] Part of last HUGE COMMIT about NCic.status --- matita/matita/matitaScript.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index f1b20efe5..fafd7cdb2 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -147,7 +147,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse | thms -> String.concat ", " (HExtlib.filter_map (function - | NotationPt.NRef r -> Some (NCicPp.r2s true r) + | NotationPt.NRef r -> Some (NCicPp.r2s status true r) | _ -> None) thms) in @@ -254,7 +254,7 @@ let source_buffer = source_view#source_buffer in let similarsymbols_tag_name = "similarsymbolos" in let similarsymbols_tag = `NAME similarsymbols_tag_name in let initial_statuses current baseuri = - let status = new GrafiteTypes.status baseuri in + let status = new MatitaEngine.status baseuri in (match current with Some current -> NCicLibrary.time_travel status; -- 2.39.2