X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.mli;h=e47ddc35fd1b65c5770e74fef64eb38b5c83a6bb;hb=3ed50d510dbab127125a8af9f72554c2dec72ef5;hp=831878d42e1d02106d6cf51fa25445fffbb50cec;hpb=6afdc65fcdb592dccb751849f65b1f482ef97cd6;p=goals.git

diff --git a/src/ast.mli b/src/ast.mli
index 831878d..e47ddc3 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -45,13 +45,13 @@ and pattern =
   | PTactic of loc * id * substs list
 and expr =
   (** goal (params) = patterns : exprs code *)
-  | EGoal of loc * goal
+  | EGoalDefn of loc * goal
   (** tactic (params) = code *)
-  | ETactic of loc * tactic
+  | ETacticDefn of loc * tactic
   (** call goalname (params) etc. *)
   | ECallGoal of loc * id * expr list
   (** call *tactic (params) etc. *)
-  | ECallTactic of loc * id * expr list
+  | ETacticCtor 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