diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 19:09:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-23 19:50:55 +0100 |
| commit | 21750c40ee3f7ef3103121db68aef4339dceba40 (patch) | |
| tree | 0d431861ae07801be81224e6123f151a24c84d41 /vernac/indschemes.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 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index e4ca98749..2f4c95aff 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -258,7 +258,7 @@ let declare_one_induction_scheme ind = let declare_induction_schemes kn = let mib = Global.lookup_mind kn in - if mib.mind_finite <> Decl_kinds.CoFinite then begin + if mib.mind_finite <> Declarations.CoFinite then begin for i = 0 to Array.length mib.mind_packets - 1 do declare_one_induction_scheme (kn,i); done; @@ -268,7 +268,7 @@ let declare_induction_schemes kn = let declare_eq_decidability_gen internal names kn = let mib = Global.lookup_mind kn in - if mib.mind_finite <> Decl_kinds.CoFinite then + if mib.mind_finite <> Declarations.CoFinite then ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn) let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) @@ -512,7 +512,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in - if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) + if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; |