(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
+type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
(** current goal, integer index *)
type goal = int
type status = proof * goal
-let initial_status ty metasenv =
+let initial_status ty metasenv attrs =
let rec aux max = function
| [] -> max + 1
| (idx, _, _) :: tl ->
aux max tl
in
let newmeta_idx = aux 0 metasenv in
+ let _subst = [] in
let proof =
- None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty
+ None, (newmeta_idx, [], ty) :: metasenv, _subst, 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
calls the opaque tactic on the status
*)
let apply_tactic t status =
- let (uri,metasenv,bo,ty), gl = t status in
+ let (uri,metasenv,subst,bo,ty, attrs), gl = t status in
match
CicRefine.pack_coercion_obj
- (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],[]))
+ (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
with
- | Cic.CurrentProof (_,metasenv,_,ty,_,_) ->
- (uri,metasenv,bo,ty), gl
+ | Cic.CurrentProof (_,metasenv,_,ty,_, attrs) ->
+ (uri,metasenv,subst,bo,ty, attrs), gl
| _ -> assert false
;;
type mk_fresh_name_type =
Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
-let goals_of_proof (_,metasenv,_,_) = List.map (fun (g,_,_) -> g) metasenv
+let goals_of_proof (_,metasenv,_subst,_,_,_) = List.map (fun (g,_,_) -> g) metasenv