X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;ds=sidebyside;f=src%2Fast.ml;h=885eefee103c1ef618eae9933b508defb5d27d00;hb=b14ff66c953e6a73e9ac2fe8d42dd68e92e58f53;hp=6a7823c16a3b526fde6a8287fd419cc6b9f8e705;hpb=318cea9f1c7669d23d27fc362bf06b9aca1b61a1;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index 6a7823c..885eefe 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -38,6 +38,7 @@ and pattern =
 and expr =
   | EGoal of loc * goal
   | ECall of loc * id * expr list
+  | ETactic of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
   | ESubsts of loc * substs
@@ -109,7 +110,7 @@ and print_def fp name expr =
 
 and print_pattern fp = function
   | PTactic (loc, name, params) ->
-     fprintf fp "%s (" name;
+     fprintf fp "*%s (" name;
      iter_with_commas fp print_substs params;
      fprintf fp ")"
   | PVar (loc, id) -> print_id fp id
@@ -120,6 +121,10 @@ and print_expr fp = function
      fprintf fp "%s (" name;
      iter_with_commas fp print_expr params;
      fprintf fp ")"
+  | ETactic (loc, name, params) ->
+     fprintf fp "*%s (" name;
+     iter_with_commas fp print_expr params;
+     fprintf fp ")"
   | EVar (loc, var) -> print_id fp var
   | EList (loc, xs) ->
      fprintf fp "[";