diff options
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 71cef59e2..c8684a9a0 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1984,7 +1984,7 @@ let rec xlate_vernac = (* xlate_formula (Option.get c1), record_constructor, *) (* build_record_field_list field_list) *) | VernacInductive (isind, _, lmi) -> - let co_or_ind = if isind then "Inductive" else "CoInductive" in + let co_or_ind = if Decl_kinds.recursivity_flag_of_kind isind then "Inductive" else "CoInductive" in let strip_mutind = function (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) -> CT_ind_spec |