X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=840a6e22017147b6a8b92587f235915b6d80edf1;hb=95eefcde41db69e3aaab3e75962c6c80c314c159;hp=1a7c0a981ac91115cde3bb1f6ad61b75d54fc13f;hpb=d4f508a277973778507021761fed85fc7d5be254;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 1a7c0a981..840a6e220 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -605,7 +605,7 @@ let record_index_eq =
  let basic_index_eq uri
    ~refresh_uri_in_universe 
    ~refresh_uri_in_term 
-   = index_eq uri 
+   = index_eq (NCicLibrary.refresh_uri uri) 
  in
   NCicLibrary.Serializer.register#run "index_eq"
    object(_ : 'a NCicLibrary.register_type)
@@ -763,6 +763,8 @@ let eval_ng_tac tac =
  let rec aux f (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
+  | GrafiteAst.NSmartApply (_loc, t) -> 
+      NnAuto.smart_apply_tac (text,prefix_len,t) 
   | GrafiteAst.NAssert (_loc, seqs) ->
      NTactics.assert_tac
       ((List.map