diff options
| author | Emilio Jesus Gallego Arias | 2020-05-20 00:47:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | d83e95cce852c5471593a27d0fdca39a262c885f (patch) | |
| tree | 9117298b6f6d0a69e6863578858de27ddb23e8ba /vernac/comAssumption.ml | |
| parent | 7d183d8a12a03a608a3dc8a724142468b45886ac (diff) | |
[declare] [api] Removal of deprecated functions
The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.
All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 44c30598aa..9c82eb8960 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -174,7 +174,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = uvars, (coe,t,imps)) Univ.LSet.empty l in - (* XXX: Using `DeclareDef.prepare_parameter` here directly is not + (* XXX: Using `Declare.prepare_parameter` here directly is not possible as we indeed declare several parameters; however, restrict_universe_context should be called in a centralized place IMO, thus I think we should adapt `prepare_parameter` to handle @@ -202,7 +202,7 @@ let context_insection sigma ~poly ctx = else Monomorphic_entry Univ.ContextSet.empty in let entry = Declare.definition_entry ~univs ~types:t b in - (* XXX Fixme: Use DeclareDef.prepare_definition *) + (* XXX Fixme: Use Declare.prepare_definition *) let uctx = Evd.evar_universe_context sigma in let kind = Decls.(IsDefinition Definition) in let _ : GlobRef.t = |