X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=e769fd7d63bf7d19958006aad47b41ec1a99bb9b;hb=50fffea30b07e377834af799cd262d6f5d5aff0c;hp=47447e49eb77268cc2bfc13dfa5fbcea1fd927bf;hpb=99246615bc3c84dfb85180869487dd6f432c1a99;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 47447e49e..e769fd7d6 100644
--- 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''