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) } as incomplete_proof) ->
+ | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
Incomplete_proof
- { incomplete_proof with proof = (uri, metasenv, proof, ty) }
+ { 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")
(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
match cmd with
| GrafiteAst.Default _
- | GrafiteAst.Index _ ->
+ | GrafiteAst.Index _
+ | GrafiteAst.Coercion _ ->
if List.mem cmd content then acc
else cmd :: acc
| _ -> cmd :: acc)