diff options
| author | Emilio Jesus Gallego Arias | 2017-12-15 19:09:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-23 19:50:55 +0100 |
| commit | 21750c40ee3f7ef3103121db68aef4339dceba40 (patch) | |
| tree | 0d431861ae07801be81224e6123f151a24c84d41 /pretyping/inductiveops.ml | |
| 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 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 34df7d3d72..78e6bc6f14 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 |