X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.mli;h=e47ddc35fd1b65c5770e74fef64eb38b5c83a6bb;hb=3ed50d510dbab127125a8af9f72554c2dec72ef5;hp=56bfa7bb67bfabe5c867b7bf375839673d535134;hpb=214f84c3b07227767fef90934895a167b15113a1;p=goals.git

diff --git a/src/ast.mli b/src/ast.mli
index 56bfa7b..e47ddc3 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -26,6 +26,9 @@ module Env : sig
   val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val filter: (key -> 'a -> bool) -> 'a t -> 'a t
   val bindings: 'a t -> (key * 'a) list
+
+  (* This is not the normal Map.merge function. *)
+  val merge : 'a t -> 'a t -> 'a t
 end
 
 (** Location where we parsed from $loc = $startpos, $endpos *)
@@ -42,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 *)
@@ -110,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