aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
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