From 86ff0d02160daa8c555a08f76af5d9699a8c2b43 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 13 Apr 2012 16:49:28 +0000
Subject: 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
---
 toplevel/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 =
-- 
cgit v1.2.3