+ (** %-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 getpred : env -> loc -> id -> pred
+(** Look up a predicate in the environment. Raise [Failure _] if not
+ found or if the named variable is not a predicate. *)