+ (** %-substitution. *)
+
+val getvar : env -> loc -> id -> expr
+(** Look up a variable in the environment. Raise [Failure _]
+ if not found. *)
+
+val getgoal : env -> loc -> id -> goal
+(** Look up a goal in the environment. Raise [Failure _] if not
+ found or if the named variable is not a goal. *)
+
+val getfunc : env -> loc -> id -> func
+(** Look up a function in the environment. Raise [Failure _] if not
+ found or if the named variable is not a function. *)
+
+val gettactic : env -> loc -> id -> tactic
+(** Look up a tactic in the environment. Raise [Failure _] if not
+ found or if the named variable is not a tactic. *)