diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 10:19:29 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 10:19:29 +0100 |
| commit | f6857ce53ecf64b0086854495b4a8451f476d5b4 (patch) | |
| tree | 7c36a59b64fcd20b3666eca8de54b4fd33606cc1 /pretyping | |
| parent | 4969f9425cb0d5cd5bd735110886a0cbd2641588 (diff) | |
| parent | 21750c40ee3f7ef3103121db68aef4339dceba40 (diff) | |
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 6 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
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 |