aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-15 19:09:15 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-23 19:50:55 +0100
commit21750c40ee3f7ef3103121db68aef4339dceba40 (patch)
tree0d431861ae07801be81224e6123f151a24c84d41 /pretyping
parentdea75d74c222c25f6aa6c38506ac7a51b339e9c6 (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 'pretyping')
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/inductiveops.ml6
-rw-r--r--pretyping/unification.ml2
3 files changed, 5 insertions, 5 deletions
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