From 3c29ea3b2e58a7f76195834e9ab43d7e99a0a323 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 3 Sep 2014 18:22:58 +0200
Subject: Factorize the parsing rules of [Record] and the other kind of type
 definitions.

They were almost identical, except some unused misplaced coercion symbol in the non-[Record] rule.
---
 parsing/g_vernac.ml4 | 29 ++++++++++-------------------
 1 file changed, 10 insertions(+), 19 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f7f049884b..9fb7c89261 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -220,17 +220,6 @@ GEXTEND Gram
   ] ]
   ;
 
-  gallina_ext:
-    [ [ priv = private_token; 
-	b = record_token; oc = opt_coercion; name = identref;
-        ps = binders;
-	s = OPT [ ":"; s = lconstr -> s ];
-	cfs = [ ":="; l = constructor_list_or_record_decl -> l
-	  | -> RecordDecl (None, []) ] ->
-	  let (recf,indf) = b in
-	    VernacInductive (priv,indf,[((oc,name),ps,s,recf,cfs),[]])
-  ] ]
-  ;
   thm_token:
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
@@ -270,16 +259,14 @@ GEXTEND Gram
   finite_token:
     [ [ "Inductive" -> (Inductive_kw,Finite)
       | "CoInductive" -> (CoInductive,CoFinite)
-      | "Variant" -> (Variant,BiFinite) ] ]
+      | "Variant" -> (Variant,BiFinite)
+      | IDENT "Record" -> (Record,BiFinite)
+      | IDENT "Structure" -> (Structure,BiFinite)
+      | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
   ;
-  record_token:
-    [ [ IDENT "Record" -> (Record,BiFinite)
-      | IDENT "Structure" -> (Structure,BiFinite)
-      | IDENT "Class" -> (Class true,BiFinite) ] ]
-  ;
   (* Simple definitions *)
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
@@ -304,10 +291,14 @@ GEXTEND Gram
     | -> [] ] ]
   ;
   (* Inductives and records *)
+  opt_constructors_or_fields:
+    [ [ ":="; lc = constructor_list_or_record_decl -> lc
+      | -> RecordDecl (None, []) ] ]
+  ;
   inductive_definition:
-    [ [ id = identref; oc = opt_coercion; indpar = binders;
+    [ [ oc = opt_coercion; id = identref; indpar = binders;
         c = OPT [ ":"; c = lconstr -> c ];
-        ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
+        lc=opt_constructors_or_fields; ntn = decl_notation ->
 	   (((oc,id),indpar,c,lc),ntn) ] ]
   ;
   constructor_list_or_record_decl:
-- 
cgit v1.2.3