diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 19:09:15 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-23 19:50:55 +0100 |
commit | 21750c40ee3f7ef3103121db68aef4339dceba40 (patch) | |
tree | 0d431861ae07801be81224e6123f151a24c84d41 /kernel | |
parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) |
[api] Also deprecate constructors of Decl_kinds.
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cClosure.ml | 2 | ||||
-rw-r--r-- | kernel/indtypes.ml | 2 | ||||
-rw-r--r-- | kernel/inductive.ml | 4 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 2 | ||||
-rw-r--r-- | kernel/subtyping.ml | 2 |
5 files changed, 6 insertions, 6 deletions
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 |