diff options
| author | Emilio Jesus Gallego Arias | 2020-11-16 04:05:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2021-02-25 20:55:20 +0100 |
| commit | d866ed978ece3b80364dfcf67ee801a556462f29 (patch) | |
| tree | aa11a82739c65d6b54d220485d4131e561ee0f91 /vernac/declare.mli | |
| parent | 24e94b3dac66510e6d57b9f55f9a4e3e84fd6e54 (diff) | |
[proof using] Remove duplicate code, refactor.
PR #13183 introduced quite a bit of duplicate code, we refactor it and
expose less internals on the way. That should make the API more
robust.
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index 37a61cc4f0..81558e6f6b 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -79,7 +79,7 @@ module CInfo : sig -> typ:'constr -> ?args:Name.t list -> ?impargs:Impargs.manual_implicits - -> ?using:Names.Id.Set.t + -> ?using:Proof_using.t -> unit -> 'constr t @@ -244,7 +244,7 @@ module Proof : sig (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) *) - val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t + val set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t (** Gets the set of variables declared to be used by the proof. None means no "Proof using" or #[using] was given *) |