aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli16
-rw-r--r--interp/declare.ml2
-rw-r--r--interp/dumpglob.ml3
-rw-r--r--intf/decl_kinds.ml3
-rw-r--r--kernel/cClosure.ml2
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--parsing/g_vernac.ml41
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml6
-rw-r--r--plugins/funind/merge.ml8
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/inductiveops.ml6
-rw-r--r--pretyping/unification.ml2
-rw-r--r--printing/prettyp.ml4
-rw-r--r--printing/printmod.ml6
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--tactics/tactics.ml2
-rw-r--r--vernac/auto_ind_decl.ml2
-rw-r--r--vernac/comInductive.ml3
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/record.ml4
25 files changed, 51 insertions, 45 deletions
diff --git a/API/API.mli b/API/API.mli
index 24a99d57f..84c15238a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1443,9 +1443,9 @@ sig
type record_body = (Id.t * Constant.t array * projection_body array) option
type recursivity_kind =
- | Finite
- | CoFinite
- | BiFinite
+ | Finite (** = inductive *)
+ | CoFinite (** = coinductive *)
+ | BiFinite (** = non-recursive, like in "Record" definitions *)
type mutual_inductive_body = {
mind_packets : one_inductive_body array;
@@ -2160,10 +2160,14 @@ module Decl_kinds :
sig
type polymorphic = bool
type cumulative_inductive_flag = bool
+
type recursivity_kind = Declarations.recursivity_kind =
- | Finite
- | CoFinite
- | BiFinite
+ | Finite (** = inductive *)
+ [@ocaml.deprecated "Please use [Declarations.Finite"]
+ | CoFinite (** = coinductive *)
+ [@ocaml.deprecated "Please use [Declarations.CoFinite"]
+ | BiFinite (** = non-recursive, like in "Record" definitions *)
+ [@ocaml.deprecated "Please use [Declarations.BiFinite"]
[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
type discharge =
diff --git a/interp/declare.ml b/interp/declare.ml
index 5be07e09e..d1b79ffcd 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -349,7 +349,7 @@ let dummy_one_inductive_entry mie = {
let dummy_inductive_entry (_,m) = ([],{
mind_entry_params = [];
mind_entry_record = None;
- mind_entry_finite = Decl_kinds.BiFinite;
+ mind_entry_finite = Declarations.BiFinite;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
mind_entry_private = None;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 0197cf9ae..d7962e29a 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -68,6 +68,7 @@ let pause () = previous_state := !glob_output; glob_output := NoGlob
let continue () = glob_output := !previous_state
open Decl_kinds
+open Declarations
let type_of_logical_kind = function
| IsDefinition def ->
@@ -111,14 +112,12 @@ let type_of_global_ref gr =
| Globnames.IndRef ind ->
let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
if mib.Declarations.mind_record <> None then
- let open Decl_kinds in
begin match mib.Declarations.mind_finite with
| Finite -> "indrec"
| BiFinite -> "rec"
| CoFinite -> "corec"
end
else
- let open Decl_kinds in
begin match mib.Declarations.mind_finite with
| Finite -> "ind"
| BiFinite -> "variant"
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index b0c1f6661..b9a3f0c21 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -77,6 +77,9 @@ type logical_kind =
type recursivity_kind = Declarations.recursivity_kind =
| Finite (** = inductive *)
+ [@ocaml.deprecated "Please use [Declarations.Finite"]
| CoFinite (** = coinductive *)
+ [@ocaml.deprecated "Please use [Declarations.CoFinite"]
| BiFinite (** = non-recursive, like in "Record" definitions *)
+ [@ocaml.deprecated "Please use [Declarations.BiFinite"]
[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 31ded9129..11616da7b 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -810,7 +810,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
| Some (Some (_,projs,pbs)) when
- mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
+ mib.Declarations.mind_finite == Declarations.BiFinite ->
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8e9b606a5..1f2ae0b6c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -710,7 +710,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
best-effort fashion. *)
let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
let ntypes = Array.length inds in
- let recursive = finite != Decl_kinds.BiFinite in
+ let recursive = finite != BiFinite in
let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
let ra_env_ar = Array.rev_to_list rc in
let nparamsctxt = Context.Rel.length paramsctxt in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2a629f00a..28a09b81b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -38,14 +38,14 @@ let find_inductive env c =
let (t, l) = decompose_app (whd_all env c) in
match kind t with
| Ind ind
- when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
+ when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l)
| _ -> raise Not_found
let find_coinductive env c =
let (t, l) = decompose_app (whd_all env c) in
match kind t with
| Ind ind
- when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
+ when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l)
| _ -> raise Not_found
let inductive_params (mib,_) = mib.mind_nparams
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index de4dc2107..160a90dc2 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -515,7 +515,7 @@ let rec lambda_of_constr env sigma c =
{ asw_ind = ind;
asw_ci = ci;
asw_reloc = tbl;
- asw_finite = mib.mind_finite <> Decl_kinds.CoFinite;
+ asw_finite = mib.mind_finite <> CoFinite;
asw_prefix = prefix}
in
(* translation of the argument *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2913c6dfa..d0d5cb1d5 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -193,7 +193,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
(arities_of_specif (mind, inst) (mib2, p2))
in
let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
- check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
+ check (fun mib -> mib.mind_finite<>CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x);
assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps);
assert (Array.length mib1.mind_packets >= 1
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c18c6810f..29bcddaf4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,6 +15,7 @@ open Constrexpr_ops
open Extend
open Vernacexpr
open Decl_kinds
+open Declarations
open Misctypes
open Tok (* necessary for camlp4 *)
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)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f7a3789a2..788e4d268 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1044,7 +1044,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
+ | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
let pars = mib.Declarations.mind_nparams in
(try
let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 34df7d3d7..78e6bc6f1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -275,7 +275,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
let has_dependent_elim mib =
match mib.mind_record with
- | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+ | Some (Some _) -> mib.mind_finite == BiFinite
| _ -> true
(* Annotation for cases *)
@@ -486,7 +486,7 @@ let find_inductive env sigma c =
let (t, l) = decompose_app sigma (whd_all env sigma c) in
match EConstr.kind sigma t with
| Ind ind
- when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
+ when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite ->
let l = List.map EConstr.Unsafe.to_constr l in
(ind, l)
| _ -> raise Not_found
@@ -496,7 +496,7 @@ let find_coinductive env sigma c =
let (t, l) = decompose_app sigma (whd_all env sigma c) in
match EConstr.kind sigma t with
| Ind ind
- when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
+ when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite ->
let l = List.map EConstr.Unsafe.to_constr l in
(ind, l)
| _ -> raise Not_found
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 30674fee2..b41fb4e4d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -666,7 +666,7 @@ let is_eta_constructor_app env sigma ts f l1 term =
| Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite &&
+ | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
(** Check that the other term is neutral *)
is_neutral env sigma ts term
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 647111bbe..2b7886d11 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -235,8 +235,8 @@ let print_type_in_type ref =
let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
let eta = match recflag with
- | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion"
- | Decl_kinds.BiFinite -> str " with eta conversion"
+ | CoFinite | Finite -> str" without eta conversion"
+ | BiFinite -> str " with eta conversion"
in
[Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
| _ -> []
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 05292b06b..fb9d45a79 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -125,7 +125,7 @@ let print_mutual_inductive env mind mib udecl =
let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
in
let keyword =
- let open Decl_kinds in
+ let open Declarations in
match mib.mind_finite with
| Finite -> "Inductive"
| BiFinite -> "Variant"
@@ -184,7 +184,7 @@ let print_record env mind mib udecl =
(Array.to_list (Univ.Instance.to_array u)) udecl in
let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
let keyword =
- let open Decl_kinds in
+ let open Declarations in
match mib.mind_finite with
| BiFinite -> "Record"
| Finite -> "Inductive"
@@ -346,7 +346,7 @@ let print_body is_impl env mp (l,body) =
pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
with e when CErrors.noncritical e ->
let keyword =
- let open Decl_kinds in
+ let open Declarations in
match mib.mind_finite with
| Finite -> def "Inductive"
| BiFinite -> def "Variant"
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 2c8ca1972..a3a3e0a9e 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -48,7 +48,7 @@ let match_with_non_recursive_type sigma t =
let (hdapp,args) = decompose_app sigma t in
(match EConstr.kind sigma hdapp with
| Ind (ind,u) ->
- if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then
+ if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then
Some (hdapp,args)
else
None
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 508040ec1..4ee0a8a7b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1492,7 +1492,7 @@ let simplest_ecase c = general_case_analysis true None (c,NoBindings)
exception IsNonrec
-let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Decl_kinds.BiFinite
+let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite
let find_ind_eliminator ind s gl =
let gr = lookup_eliminator ind s in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 51dd5cd4f..ec6b62ee2 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -317,7 +317,7 @@ let build_beq_scheme mode kn =
let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
if not (Sorts.List.mem InSet kelim) then
raise (NonSingletonProp (kn,i));
- if mib.mind_finite = Decl_kinds.CoFinite then
+ if mib.mind_finite = CoFinite then
raise NoDecidabilityCoInductive;
let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
create_input fix),
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f3f50f41d..1c8677e9c 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -25,7 +25,6 @@ open Nametab
open Impargs
open Reductionops
open Indtypes
-open Decl_kinds
open Pretyping
open Evarutil
open Indschemes
@@ -411,7 +410,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
(* spiwack: raises an error if the structure is supposed to be non-recursive,
but isn't *)
begin match mie.mind_entry_finite with
- | BiFinite when is_recursive mie ->
+ | Declarations.BiFinite when is_recursive mie ->
if Option.has_some mie.mind_entry_record then
user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
else
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e4ca98749..2f4c95aff 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -258,7 +258,7 @@ let declare_one_induction_scheme ind =
let declare_induction_schemes kn =
let mib = Global.lookup_mind kn in
- if mib.mind_finite <> Decl_kinds.CoFinite then begin
+ if mib.mind_finite <> Declarations.CoFinite then begin
for i = 0 to Array.length mib.mind_packets - 1 do
declare_one_induction_scheme (kn,i);
done;
@@ -268,7 +268,7 @@ let declare_induction_schemes kn =
let declare_eq_decidability_gen internal names kn =
let mib = Global.lookup_mind kn in
- if mib.mind_finite <> Decl_kinds.CoFinite then
+ if mib.mind_finite <> Declarations.CoFinite then
ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
@@ -512,7 +512,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
let declare_default_schemes kn =
let mib = Global.lookup_mind kn in
let n = Array.length mib.mind_packets in
- if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+ if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag)
&& mib.mind_typing_flags.check_guarded then
declare_induction_schemes kn;
if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 27a680b9b..6ef310837 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -100,7 +100,7 @@ let find_mutually_recursive_statements sigma thms =
match EConstr.kind sigma t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- mind.mind_finite <> Decl_kinds.CoFinite ->
+ mind.mind_finite <> Declarations.CoFinite ->
[ind,x,i]
| _ ->
[]) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in
@@ -110,7 +110,7 @@ let find_mutually_recursive_statements sigma thms =
match EConstr.kind sigma whnf_ccl with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
+ Int.equal mind.mind_ntypes n && mind.mind_finite == Declarations.CoFinite ->
[ind,x,0]
| _ ->
[] in
diff --git a/vernac/record.ml b/vernac/record.ml
index 114b55cb4..fb73f3a01 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -143,7 +143,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
let assums = List.filter is_local_assum newps in
let params = List.map (RelDecl.get_name %> Name.get_id) assums in
- let ty = Inductive (params,(finite != BiFinite)) in
+ let ty = Inductive (params,(finite != Declarations.BiFinite)) in
let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
let env2,sigma,impls,newfs,data =
interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
@@ -507,7 +507,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
- let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
+ let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls
params arity template fieldimpls fields
~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 03:06:49 +0000