(**
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 (fun _ m u -> t, m, u)
+ | 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, restoring the original
- universe graph if the tactic Fails
+ calls the opaque tactic on the status
*)
let apply_tactic t status =
- t status
+ let (uri,metasenv,subst,bo,ty, attrs), gl = t status in
+ match
+ CicRefine.pack_coercion_obj
+ (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
+ with
+ | Cic.CurrentProof (_,metasenv,_,ty,_, attrs) ->
+ (uri,metasenv,subst,bo,ty, attrs), gl
+ | _ -> assert false
+;;
(** constraint: the returned value will always be constructed by Cic.Name **)
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