diff options
| author | aspiwack | 2012-04-13 16:49:28 +0000 |
|---|---|---|
| committer | aspiwack | 2012-04-13 16:49:28 +0000 |
| commit | 86ff0d02160daa8c555a08f76af5d9699a8c2b43 (patch) | |
| tree | 41676c844b76f33ad7e3f260d409950f4389af9d | |
| parent | f5c248adbc984b8bb5b22821c1812acf91ad30ee (diff) | |
Better error message when defining recursive records with Record or
Structure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15159 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 = |