let get_proof_metasenv status =
match status.proof_status with
| No_proof -> []
- | Proof (_, metasenv, _, _, _)
- | Incomplete_proof { proof = (_, metasenv, _, _, _) }
+ | Proof (_, metasenv, _, _, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) }
| Intermediate metasenv ->
metasenv
let proof_status =
match status.proof_status with
| No_proof -> Intermediate metasenv
- | Incomplete_proof ({ proof = (uri, _, proof, ty, attrs) } as incomplete_proof) ->
+ | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
Incomplete_proof
- { incomplete_proof with proof = (uri, metasenv, proof, ty, attrs) }
+ { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) }
| Intermediate _ -> Intermediate metasenv
- | Proof (_, metasenv', _, _, _) ->
+ | Proof (_, metasenv', _, _, _, _) ->
assert (metasenv = metasenv');
status.proof_status
in
let get_proof_context status goal =
match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _, _) } ->
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
context
| _ -> []
let get_proof_conclusion status goal =
match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _, _) } ->
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
conclusion
| _ -> raise (Statement_error "no ongoing proof")