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 *)
| 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
+ | ETacticConstructor of loc * id * expr list
(** variable, or goal call with no parameters *)
| EVar of loc * id
(** list *)