From d83e95cce852c5471593a27d0fdca39a262c885f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 20 May 2020 00:47:21 +0200
Subject: [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.
---
 vernac/comInductive.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'vernac/comInductive.ml')

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
-- 
cgit v1.2.3