diff options
| author | Maxime Dénès | 2019-04-29 16:38:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-29 16:38:26 +0200 |
| commit | f08880552350310df8a60ec37d6ada9d0ef1b40f (patch) | |
| tree | 3af1ff908cd64f00ec0c871a780449f9a5de529c /toplevel | |
| parent | 2ad60e808052d163ca84094131b453f2bccc3143 (diff) | |
| parent | 45684eb8f1202665dc33bd98f1dbd46ae572757e (diff) | |
Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ccompile.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
3 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 416ea88c1b..8934385091 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -85,7 +85,7 @@ let ensure_exists f = 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 () in + let pfs = Vernacstate.Proof_global.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 4129562065..087cd67f3a 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -194,6 +194,7 @@ let make_prompt () = (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ())) ^ " < " with Vernacstate.Proof_global.NoCurrentProof -> "Coq < " + [@@ocaml.warning "-3"] (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global @@ -363,6 +364,7 @@ let top_goal_print ~doc c oldp newp = let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer + [@@ocaml.warning "-3"] let exit_on_error = let open Goptions in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 038ff54bf6..6c6379ec5e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,7 +70,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 () in + let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird |