Added ntry and nassumption tactics

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 65b6683ebc384e107331a0c42c51a5f0a9ca323b..e02bd159fe0d13544c5cc33252810b2d5bdcff0e 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -603,7 +603,7 @@ let eval_ng_punct (_text, _prefix_len, punct) =
   | GrafiteAst.Merge _ -> NTactics.merge_tac 
 ;;
 
-let eval_ng_tac (text, prefix_len, tac) =
+let rec eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
   | GrafiteAst.NAssert (_loc, seqs) ->
@@ -654,6 +654,9 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NSkip _ -> NTactics.skip_tac
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
+  | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
+      (eval_ng_tac (text, prefix_len, tac))
+  | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
 ;;
       
 let subst_metasenv_and_fix_names s =