alias diffing/insertion is now handled by matitaEngine (invoked both

[helm.git] / helm / matita / matitacLib.ml

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 47447e49eb77268cc2bfc13dfa5fbcea1fd927bf..e769fd7d63bf7d19958006aad47b41ec1a99bb9b 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -27,6 +27,8 @@ open Printf
 
 open GrafiteTypes
 
+exception AttemptToInsertAnAlias
+
 let pp_ast_statement =
   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
     ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
@@ -60,8 +62,11 @@ let run_script is eval_function  =
         HLog.debug ("Executing: ``" ^ stm ^ "''"))
   in
   try
-   let lexicon_status'', grafite_status'' =
-    eval_function lexicon_status' grafite_status' is cb
+   let grafite_status'', lexicon_status'' =
+    match eval_function lexicon_status' grafite_status' is cb with
+       [] -> assert false
+     | (s,None)::_ -> s
+     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
    in
     lexicon_status := Some lexicon_status'';
     grafite_status := Some grafite_status''