git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Define *file() syntax for tactic constructors.
[goals.git]
/
src
/
ast.ml
diff --git
a/src/ast.ml
b/src/ast.ml
index
6a7823c
..
885eefe
100644
(file)
--- 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
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
| 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) ->
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
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 ")"
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 "[";
| EVar (loc, var) -> print_id fp var
| EList (loc, xs) ->
fprintf fp "[";