diff options
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 51dd5cd4f..ec6b62ee2 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -317,7 +317,7 @@ let build_beq_scheme mode kn = let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in if not (Sorts.List.mem InSet kelim) then raise (NonSingletonProp (kn,i)); - if mib.mind_finite = Decl_kinds.CoFinite then + if mib.mind_finite = CoFinite then raise NoDecidabilityCoInductive; let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), |