options: options;
objects: UriManager.uri list;
coercions: UriManager.uri list;
+ universe:Universe.universe;
}
let get_current_proof status =
match status.proof_status with
| Incomplete_proof { proof = p } -> p
+ | Proof p -> p
| _ -> raise (Statement_error "no ongoing proof")
let get_proof_metasenv status =
(fun cmd acc ->
(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
match cmd with
- | GrafiteAst.Default _ ->
+ | GrafiteAst.Default _
+ | GrafiteAst.Index _ ->
if List.mem cmd content then acc
else cmd :: acc
| _ -> cmd :: acc)