Matitaweb:

[helm.git] / matitaB / components / grafite_engine / grafiteEngine.ml

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index 5ac28559dc5482ec4182cb48463e33023e8b3b0a..2021114853c7368a86fc5512715d69b814837812 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -604,7 +604,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                 else
                   nstatus
                with
-               | MultiPassDisambiguator.DisambiguationError _
+               | GrafiteDisambiguate.Error _
                | NCicTypeChecker.TypeCheckerFailure _ ->
                   (*HLog.warn "error in generating projection/eliminator";*)
                   status
@@ -659,7 +659,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                       status (name,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
                   eval_alias status (mode,aliases)
-               with MultiPassDisambiguator.DisambiguationError _-> 
+               with GrafiteDisambiguate.Error _ -> 
                  HLog.warn ("error in generating coercion: "^name);
                  status) 
              status coercions
@@ -830,6 +830,7 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
         List.fold_left 
           (fun status tac ->
             let status = eval_ng_tac (text,prefix_len,tac) status in
+            prerr_endline "prima di subst_metasenv_and_fix_names";
             subst_metasenv_and_fix_names status)
           status tacl
        in