X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ca02263b01e6de6aceeff38012aa5e98be2e573a;hb=c450fdfb1b02eb69e5e7ef25f0acdf80157710df;hp=c44b70178fafd36a9069372807fa8e3dd4554a48;hpb=102cb2ba885b9fa93c824c7c07ba2467cfec0e16;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c44b70178..ca02263b0 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -777,10 +777,11 @@ let eval_ng_tac tac =
            ) hyps,
           (text,prefix_len,concl))
        ) seqs)
-  | GrafiteAst.NAuto (_loc, (None,a)) -> NAuto.auto_tac ~params:(None,a)
+  | GrafiteAst.NAuto (_loc, (None,a)) -> 
+      NAuto.auto_tac ~params:(None,a) ?trace_ref:None
   | GrafiteAst.NAuto (_loc, (Some l,a)) ->
       NAuto.auto_tac
-	~params:(Some List.map (fun x -> "",0,x) l,a)
+	~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
@@ -796,7 +797,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
 (*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
   | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
-  | GrafiteAst.NDestruct _ -> NDestructTac.destruct_tac
+  | GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -807,6 +808,7 @@ let eval_ng_tac tac =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
   | GrafiteAst.NInversion (_loc, what, where) ->
       NTactics.inversion_tac 
         ~what:(text,prefix_len,what)
@@ -829,7 +831,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
-      (aux f (text, prefix_len, tac))
+      (f f (text, prefix_len, tac))
   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
   | GrafiteAst.NBlock (_,l) -> 
       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
@@ -886,6 +888,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
+        (*prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);*)
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let index_obj =
@@ -897,7 +900,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let status =
          if index_obj then
           let status = index_obj_for_auto status obj in
-           index_eq_for_auto status uri
+           (try index_eq_for_auto status uri
+           with _ -> status)
          else
           status in
 (*