refresh uri

applyS

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 1a7c0a981ac91115cde3bb1f6ad61b75d54fc13f..840a6e22017147b6a8b92587f235915b6d80edf1 100644 (file)
--- 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