diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index b422e67b1..7db71c097 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -232,7 +232,7 @@ let declare_one_induction_scheme ind = let declare_induction_schemes kn = let mib = Global.lookup_mind kn in - if mib.mind_finite then begin + if mib.mind_finite <> Decl_kinds.CoFinite then begin for i = 0 to Array.length mib.mind_packets - 1 do declare_one_induction_scheme (kn,i); done; @@ -242,7 +242,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 then + if mib.mind_finite <> Decl_kinds.CoFinite then ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn) let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) |