Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.

3 files changed, 8 insertions, 8 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 4ae875cd7..c169b7b50 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -431,7 +431,7 @@ and extract_really_ind env kn mib =
 	let ip = (kn, 0) in
 	let r = IndRef ip in
 	if is_custom r then raise (I Standard);
-	if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive);
+        if mib.mind_finite == CoFinite then raise (I Coinductive);
 	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
 	let p,u = packets.(0) in
 	if p.ip_logical then raise (I Standard);
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 97066e531..b4e17c5d1 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1498,7 +1498,7 @@ let do_build_inductive
   try
     with_full_print
       (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
-      Decl_kinds.Finite
+      Declarations.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
@@ -1509,7 +1509,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1524,7 +1524,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 9fcb35f89..8f5d3f22f 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -20,10 +20,10 @@ open Names
 open Term
 open Constr
 open Vars
-open Declarations
 open Glob_term
 open Glob_termops
 open Decl_kinds
+open Declarations
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -353,8 +353,8 @@ let ind2name = Id.of_string "__ind2"
     be co-inductive, and for the moment they must not be mutual
     either. *)
 let verify_inds mib1 mib2 =
-  if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive";
-  if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive";
+  if mib1.mind_finite == CoFinite then error "First argument is coinductive";
+  if mib2.mind_finite == CoFinite then error "Second argument is coinductive";
   if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual";
   if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual";
   ()
@@ -891,7 +891,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   (* Declare inductive *)
   let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in
   let mie,pl,impls = ComInductive.interp_mutual_inductive indl []
-          false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
+          false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls)