diff options
| -rw-r--r-- | toplevel/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 5ed6c45c5a..ed57bfc495 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -264,7 +264,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls begin match finite with | BiFinite -> if Termops.dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then - error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record." + error "Records declared with the keyword Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." | _ -> () end; let mie = |