diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ccompile.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
3 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index a7a9b77b56..c8b8660b92 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -131,7 +131,7 @@ let set_options = List.iter set_option let compile opts copts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = - let pfs = Vernacstate.Proof_global.get_all_proof_names () [@ocaml.warning "-3"] in + let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in if not (CList.is_empty pfs) then fatal_error (str "There are pending proofs: " ++ (pfs diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index b8acdd3af1..2c5faa4df7 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -191,8 +191,8 @@ end from cycling. *) let make_prompt () = try - (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ())) ^ " < " - with Vernacstate.Proof_global.NoCurrentProof -> + (Names.Id.to_string (Vernacstate.Declare.get_current_proof_name ())) ^ " < " + with Vernacstate.Declare.NoCurrentProof -> "Coq < " [@@ocaml.warning "-3"] @@ -352,7 +352,7 @@ let print_anyway c = let top_goal_print ~doc c oldp newp = try let proof_changed = not (Option.equal cproof oldp newp) in - let print_goals = proof_changed && Vernacstate.Proof_global.there_are_pending_proofs () || + let print_goals = proof_changed && Vernacstate.Declare.there_are_pending_proofs () || print_anyway c in if not !Flags.quiet && print_goals then begin let dproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in @@ -375,7 +375,7 @@ let exit_on_error = point we should consolidate the code *) let show_proof_diff_to_pp pstate = let p = Option.get pstate in - let sigma, env = Pfedit.get_proof_context p in + let sigma, env = Proof.get_proof_context p in let pprf = Proof.partial_proof p in Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf @@ -392,7 +392,7 @@ let show_proof_diff_cmd ~state removed = let show_removed = Some removed in Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp with - | Pfedit.NoSuchGoal + | Proof.NoSuchGoal _ | Option.IsNone -> n_pp | Pp_diff.Diff_Failure msg -> begin (* todo: print the unparsable string (if we know it) *) @@ -403,7 +403,7 @@ let show_proof_diff_cmd ~state removed = else n_pp with - | Pfedit.NoSuchGoal + | Proof.NoSuchGoal _ | Option.IsNone -> CErrors.user_err (str "No goals to show.") diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 076796468f..c4c8492a4a 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -66,7 +66,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = (* Force the command *) let ndoc = if check then Stm.observe ~doc nsid else doc in - let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in + let new_proof = Vernacstate.Declare.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> let (reraise, info) = Exninfo.capture reraise in |