type lazy_pattern = (Cic.term, Cic.lazy_term) pattern
+let hole = Cic.Implicit (Some `Hole)
+
let conclusion_pattern t =
let t' =
match t with
| None -> None
| Some t -> Some (const_lazy_term t)
in
- t',[],Some (Cic.Implicit (Some `Hole))
+ t',[], Some hole
(** tactic failure *)
exception Fail of string Lazy.t