((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
;;
-let build_goal_proof l initial ty =
- let proof =
- List.fold_left
- (fun current_proof (pos,id,subst,pred) ->
- let p,l,r = proof_of_id id in
- let p = build_proof_term p in
- let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
- build_proof_step subst current_proof p pos l r pred)
- initial l
+let build_goal_proof l initial ty se =
+ let se = List.map (fun i -> Cic.Meta (i,[])) se in
+ let proof,se =
+ let rec aux se current_proof = function
+ | [] -> current_proof,se
+ | (pos,id,subst,pred)::tl ->
+ let p,l,r = proof_of_id id in
+ let p = build_proof_term p in
+ let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+ let proof = build_proof_step subst current_proof p pos l r pred in
+ let proof,se = aux se proof tl in
+ Subst.apply_subst subst proof,
+ List.map (fun x -> Subst.apply_subst subst x) se
+ in
+ aux se initial l
in
- proof
- (*canonical (contextualize_rewrites proof ty)*)
+ canonical (contextualize_rewrites proof ty), se
;;
let refl_proof ty term =
ty; term]
;;
-let metas_of_proof p =
- Utils.metas_of_term (build_proof_term p)
+let metas_of_proof p =
+ let p = build_proof_term p in
+ Utils.metas_of_term p
;;
let relocate newmeta menv =
let fix_proof = function
| Exact p -> Exact (Subst.apply_subst subst p)
| Step (s,(r,id1,(pos,id2),pred)) ->
- Step (Subst.concat_substs s subst,(r,id1,(pos,id2), pred))
+ Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
in
let p = fix_proof p in
let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in