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/proof_using.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/proof_using.mli')
| -rw-r--r-- | vernac/proof_using.mli | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 93dbd33ae4..60db4d60e6 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -10,10 +10,17 @@ (** Utility code for section variables handling in Proof using... *) -val process_expr : - Environ.env -> Evd.evar_map -> - Vernacexpr.section_subset_expr -> EConstr.types list -> - Names.Id.t list +(** At some point it would be good to make this abstract *) +type t = Names.Id.Set.t + +(** Process a [using] expression in definitions to provide the list of + used terms *) +val definition_using + : Environ.env + -> Evd.evar_map + -> using:Vernacexpr.section_subset_expr + -> terms:EConstr.constr list + -> t val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit |