From e7b29adca3c2ff636ff277dab843d517894f3bf6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Nov 2019 09:32:06 +0100
Subject: Grammar: mini-factorization between fix/cofix and
 Fixpoint/CoFixpoint.

---
 vernac/g_vernac.mlg | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a78f4645c2..d534c107f1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -437,22 +437,18 @@ GRAMMAR EXTEND Gram
   rec_definition:
     [ [ id_decl = ident_decl;
 	bl = binders_fixannot;
-        rtype = rec_type_cstr;
+        rtype = type_cstr;
         body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation ->
           { let binders, rec_order = bl in
             {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
           } ] ]
   ;
   corec_definition:
-    [ [ id_decl = ident_decl; binders = binders; rtype = rec_type_cstr;
+    [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
         body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation ->
         { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
         } ]]
   ;
-  rec_type_cstr:
-    [ [ ":"; c=lconstr -> { c }
-      | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ]
-  ;
   (* Inductive schemes *)
   scheme:
     [ [ kind = scheme_kind -> { (None,kind) }
-- 
cgit v1.2.3