| 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 *)
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