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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/idetop.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index 543ff924bd..38839f3488 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -238,7 +238,8 @@ let goals () = Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp)) end else Some (export_pre_goals Proof.(data newp) process_goal) - with Vernacstate.Proof_global.NoCurrentProof -> None;; + with Vernacstate.Proof_global.NoCurrentProof -> None + [@@ocaml.warning "-3"];; let evars () = try @@ -251,6 +252,7 @@ let evars () = let el = List.map map_evar exl in Some el with Vernacstate.Proof_global.NoCurrentProof -> None + [@@ocaml.warning "-3"] let hints () = try @@ -264,7 +266,7 @@ let hints () = let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in Some (hint_hyps, concl_next_tac) with Vernacstate.Proof_global.NoCurrentProof -> None - + [@@ocaml.warning "-3"] (** Other API calls *) @@ -297,6 +299,7 @@ let status force = Interface.status_allproofs = allproofs; Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); } + [@@ocaml.warning "-3"] let export_coq_object t = { Interface.coq_object_prefix = t.Search.coq_object_prefix; @@ -340,6 +343,7 @@ let search flags = List.map export_coq_object (Search.interface_search ?pstate ( List.map (fun (c, b) -> (import_search_constraint c, b)) flags) ) + [@@ocaml.warning "-3"] let export_option_value = function | Goptions.BoolValue b -> Interface.BoolValue b |