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/comInductive.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/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index e490b33dde..673124296d 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -657,5 +657,3 @@ let make_cases ind = let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) mip.mind_nf_lc [] - -let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations |