+ let (meta,perforated) =
+ (* If the selected term is already a meta, we return it. *)
+ (* Otherwise, we are trying to refine a non-meta term... *)
+ match term with
+ Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
+ | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)