diff options
| author | Maxime Dénès | 2017-12-27 10:19:29 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:29 +0100 |
| commit | f6857ce53ecf64b0086854495b4a8451f476d5b4 (patch) | |
| tree | 7c36a59b64fcd20b3666eca8de54b4fd33606cc1 /kernel/subtyping.ml | |
| parent | 4969f9425cb0d5cd5bd735110886a0cbd2641588 (diff) | |
| parent | 21750c40ee3f7ef3103121db68aef4339dceba40 (diff) | |
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2913c6dfad..d0d5cb1d56 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 |