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 1aa23421137610ce4943e9159581f35106946582..2021114853c7368a86fc5512715d69b814837812 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -354,7 +354,7 @@ let eval_ng_tac tac =
        ) seqs)
   | GrafiteAst.NAuto (_loc, (None,a)) -> 
       NnAuto.auto_tac ~params:(None,a) ?trace_ref:None
-  | GrafiteAst.NAuto (_loc, (Some l,a)) ->
+  | GrafiteAst.NAuto (_loc, (Some (_,l),a)) ->
       NnAuto.auto_tac
        ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
@@ -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