From 706a4f3974c2f586ecb5d695e04e7b4f1b2e3d57 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 3 Sep 2014 16:32:12 +0200
Subject: Type definitions [Variant] and [Record] really don't accept the wrong
 kind of definition.

- [Variant] will accept variant definitions but no record definition
- [Record] will accept record definitions but no variant definition
---
 toplevel/vernacentries.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9cb88f5414..a5803a24d2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -536,6 +536,10 @@ let vernac_inductive poly lo finite infer indl =
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
   match indl with
+  | [ ( _ , _ , _ ,Record, Constructors _ ),_ ] ->
+      Errors.error "The Record keyword cannot be used to define a variant type. Use Variant instead."
+  | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
+      Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class true -> Class false | _ -> b)
 	poly finite infer id bl c oc fs
-- 
cgit v1.2.3