git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
parser: Fix longstanding bug where "()" was required after CLI targets.
[goals.git]
/
src
/
ast.mli
diff --git
a/src/ast.mli
b/src/ast.mli
index
df6c60f
..
cf776eb
100644
(file)
--- a/
src/ast.mli
+++ b/
src/ast.mli
@@
-65,11
+65,11
@@
and expr =
and constant =
| CString of string
and goal = param_decl list * pattern list * expr list * code option
and constant =
| CString of string
and goal = param_decl list * pattern list * expr list * code option
-and func = param_decl list * returning * code
+and func = param_decl list * returning *
bool *
code
and tactic = param_decl list * code
and param_decl = id (** goal/func/tactic parameter. *)
and id = string
and tactic = param_decl list * code
and param_decl = id (** goal/func/tactic parameter. *)
and id = string
-and code = substs
+and code = substs
* bool (** code + quiet flag *)
and returning = RetExpr | RetStrings | RetString
and substs = subst list
and subst =
and returning = RetExpr | RetStrings | RetString
and substs = subst list
and subst =