diff options
| author | Emilio Jesus Gallego Arias | 2020-05-03 17:30:13 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-03 17:30:13 +0200 |
| commit | 223d0ad62896ce3a8831488acec133561cc9244b (patch) | |
| tree | 35c3df149b9e2581b9465fa3c72d2eb9cab78f02 | |
| parent | eab9f3bd104f154c128955ff344eb671d0e2ec93 (diff) | |
[declare] Add deprecation notices for compat modules.
We will remove this modules and submit the overlays once the
refactoring is done as to avoid churn.
| -rw-r--r-- | plugins/funind/gen_principle.ml | 2 | ||||
| -rw-r--r-- | vernac/pfedit.ml | 6 | ||||
| -rw-r--r-- | vernac/proof_global.ml | 7 |
3 files changed, 13 insertions, 2 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 131a6a6e61..07f578d2a8 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -2199,7 +2199,7 @@ let build_scheme fas = List.iter2 (fun (princ_id, _, _) (body, types, univs, opaque) -> let (_ : Constant.t) = - let opaque = if opaque = Proof_global.Opaque then true else false in + let opaque = if opaque = Declare.Opaque then true else false in let def_entry = Declare.definition_entry ~univs ~opaque ?types body in Declare.declare_constant ~name:princ_id ~kind:Decls.(IsProof Theorem) diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml index 1b34b6ec28..e6c66ee503 100644 --- a/vernac/pfedit.ml +++ b/vernac/pfedit.ml @@ -1,13 +1,19 @@ (* Compat API / *) let get_current_context = Declare.get_current_context +[@@ocaml.deprecated "Use [Declare.get_current_context]"] let solve = Proof.solve +[@@ocaml.deprecated "Use [Proof.solve]"] let by = Declare.by +[@@ocaml.deprecated "Use [Declare.by]"] let refine_by_tactic = Proof.refine_by_tactic +[@@ocaml.deprecated "Use [Proof.refine_by_tactic]"] (* We don't want to export this anymore, but we do for now *) let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac = let b, t, _unis, safe, uctx = Declare.build_by_tactic ?side_eff env ~uctx ~poly ~typ tac in b, t, safe, uctx +[@@ocaml.deprecated "Use [Proof.build_by_tactic]"] let build_constant_by_tactic = Declare.build_constant_by_tactic +[@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"] diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml index b6c07042e2..54d1db44a4 100644 --- a/vernac/proof_global.ml +++ b/vernac/proof_global.ml @@ -1,7 +1,12 @@ (* compatibility module; can be removed once we agree on the API *) type t = Declare.Proof.t +[@@ocaml.deprecated "Use [Declare.Proof.t]"] let map_proof = Declare.Proof.map_proof +[@@ocaml.deprecated "Use [Declare.Proof.map_proof]"] let get_proof = Declare.Proof.get_proof +[@@ocaml.deprecated "Use [Declare.Proof.get_proof]"] -type opacity_flag = Declare.opacity_flag = Opaque | Transparent +type opacity_flag = Declare.opacity_flag = + | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"] + | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"] |