From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 8 Jan 2010 08:11:14 +0000 (+0000)
Subject: refresh uri
X-Git-Tag: make_still_working~3142
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ab389523157f09ac9f79743ee7e8d52aabca1ee;p=helm.git

refresh uri
applyS
---

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