- new library/logic/coimplication.ma uses new decompose tactic

[helm.git] / matita / matitaScript.ml

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 0e51213096292c4caf09b2b93058fbf024f8e169..12f26036b4a1c20f829090e6ee254f74ed964f0d 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -288,7 +288,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       let t_and_ty = Cic.Cast (term,ty) in
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
       [], "", parsed_text_length
-  | TA.Inline (_,suri) ->
+  | TA.Inline (_,suri,prefix) ->
      let dbd = LibraryDb.instance () in
      let uris =
       let sql_pat =