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.

---
 parsing/g_constr.mlg | 2 +-
 parsing/pcoq.ml      | 1 +
 parsing/pcoq.mli     | 1 +
 vernac/g_vernac.mlg  | 8 ++------
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index bd4ce3c5ab..b9432e3247 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -130,7 +130,7 @@ GRAMMAR EXTEND Gram
   universe_level universe_name sort sort_family
   global constr_pattern lconstr_pattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
-  record_declaration typeclass_constraint pattern appl_arg;
+  record_declaration typeclass_constraint pattern appl_arg type_cstr;
   Constr.ident:
     [ [ id = Prim.ident -> { id } ] ]
   ;
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 0a41bba8ce..734dd8ee8a 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -451,6 +451,7 @@ module Constr =
     let typeclass_constraint = Entry.create "constr:typeclass_constraint"
     let record_declaration = Entry.create "constr:record_declaration"
     let appl_arg = Entry.create "constr:appl_arg"
+    let type_cstr = Entry.create "constr:type_cstr"
   end
 
 module Module =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ca5adf8ab3..404fbdb4fd 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -197,6 +197,7 @@ module Constr :
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
     val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
+    val type_cstr : constr_expr Entry.t
   end
 
 module Module :
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