(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
+type proof =
+ UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term Lazy.t * Cic.term * Cic.attribute list
(** current goal, integer index *)
type goal = int
type status = proof * goal
let newmeta_idx = aux 0 metasenv in
let _subst = [] in
let proof =
- None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs
+ None, (newmeta_idx, [], ty) :: metasenv, _subst,
+ lazy (Cic.Meta (newmeta_idx, [])), ty, attrs
in
(proof, newmeta_idx)
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