X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=976b25b55a79f8e7c6f3659777481b1ccaa9a4de;hb=a149b1474110583ea5f47fa5bcb85554bba92f19;hp=e55df286b87b5a0d6f069bb4f7de9228cc3f00e4;hpb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index e55df286b..976b25b55 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -797,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 
@@ -888,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 =
@@ -899,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
 (*