From 2ab389523157f09ac9f79743ee7e8d52aabca1ee Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Jan 2010 08:11:14 +0000 Subject: [PATCH 1/1] refresh uri applyS --- helm/software/components/grafite_engine/grafiteEngine.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 -- 2.39.2