X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteEngine.ml;h=ff173bc37aa1d717ed3b7e32f69d26043b5a9b42;hb=4eab714a88bad2a9d8b29b5aa20465e71655e512;hp=8b83bcff0fcf3569af351757165b11b88cd3dfbc;hpb=cbcd34fe15122eb9835a5226b98be1050b097d6a;p=helm.git

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 8b83bcff0..ff173bc37 100644
--- 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? *)