Fixing (part of) #5303 (clarifications around Record/Structure/Variant).

- We fix the inconsistency of Structure and Record which according to
  doc are the same.
- We improve the error message when not using { ... } for Record or Structure.

1 files changed, 3 insertions, 3 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 41ee165ff8..6736d83293 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -570,10 +570,10 @@ let vernac_inductive poly lo finite indl =
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
   match indl with
-  | [ ( _ , _ , _ ,Record, Constructors _ ),_ ] ->
-      CErrors.error "The Record keyword cannot be used to define a variant type. Use Variant instead."
+  | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] ->
+      CErrors.error "The Record keyword is for types defined using the syntax { ... }."
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
-      CErrors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
+      CErrors.error "The Variant keyword does not support syntax { ... }."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class _ -> Class false | _ -> b)
        poly finite id bl c oc fs