added shortcut targets

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 8b83bcff0fcf3569af351757165b11b88cd3dfbc..ff173bc37aa1d717ed3b7e32f69d26043b5a9b42 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -480,15 +480,16 @@ let eval_tactical ~disambiguate_tactic status tac =
         MatitaTacticals.solve_tactics
          ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
 
-    | GrafiteAst.Skip loc -> MatitaTacticals.skip
-    | GrafiteAst.Dot loc -> MatitaTacticals.dot
-    | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
-    | GrafiteAst.Branch loc -> MatitaTacticals.branch
-    | GrafiteAst.Shift loc -> MatitaTacticals.shift
-    | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
-    | GrafiteAst.Merge loc -> MatitaTacticals.merge
-    | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
-    | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+    | GrafiteAst.Skip _loc -> MatitaTacticals.skip
+    | GrafiteAst.Dot _loc -> MatitaTacticals.dot
+    | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
+    | GrafiteAst.Branch _loc -> MatitaTacticals.branch
+    | GrafiteAst.Shift _loc -> MatitaTacticals.shift
+    | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
+    | GrafiteAst.Merge _loc -> MatitaTacticals.merge
+    | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
+    | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
+    | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
   in
   let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
   let status =  (* is proof completed? *)