-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