diff options
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 |