+ (* To allow using Rels in the user-specified candidates, we need a context
+ * but in the case where multiple goals are open, there is no single context
+ * to type the Rels. At this time, we require that Rels be typed in the
+ * context of the first selected goal *)
+ let _,ctx,_ = current_goal ~single_goal:false status in
+ let status, candidates =