X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.mli;h=406a8293bf8710f83cdf353d9b508c194f34818f;hb=ef2b2a9ce0c7ba6f05754e3da1e5e9fbbdf88d15;hp=1fee78ea036f07cec07d4735555a42351a7b7047;hpb=266aac664780e39712228dd70a8e11465298713b;p=goals.git diff --git a/src/ast.mli b/src/ast.mli index 1fee78e..406a829 100644 --- a/src/ast.mli +++ b/src/ast.mli @@ -51,7 +51,7 @@ and expr = (** call goalname (params) etc. *) | ECallGoal of loc * id * expr list (** call *tactic (params) etc. *) - | ECallTactic of loc * id * expr list + | ETacticConstructor of loc * id * expr list (** variable, or goal call with no parameters *) | EVar of loc * id (** list *) @@ -113,9 +113,8 @@ module Substs : sig val add_var : t -> string -> unit end -(** Print all definitions in an environment. *) -val print_env : out_channel -> env -> unit - (** %a formatters. *) +val print_env : out_channel -> env -> unit val string_pattern : unit -> pattern -> string val string_expr : unit -> expr -> string +val print_expr : out_channel -> expr -> unit