From a54aefa7d2296ef3908dc21087c27250387819cc Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 3 Sep 2014 18:40:49 +0200
Subject: Commands like [Inductive > X := … | … | …] raise an error message
 instead of silently ignoring the ">" syntax.

---
 toplevel/vernacentries.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index adfccb5023..b8baca9eb0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -556,7 +556,9 @@ let vernac_inductive poly lo finite indl =
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
       Errors.error "where clause not supported for (co)inductive records"
   | _ -> let unpack = function
-      | ( (_, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
+      | ( (false, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
+      | ( (true,_),_,_,_,Constructors _),_ ->
+          Errors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead."
       | _ -> Errors.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-- 
cgit v1.2.3