Rename the 2 local type_cstr nonterminals to give them unique names

2 files changed, 6 insertions, 6 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 87b9a8eea3..470782a7dc 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -263,7 +263,7 @@ GRAMMAR EXTEND Gram
           { mkProdCN ~loc bl c }
       | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
           { mkLambdaCN ~loc bl c }
-      | "let"; id=name; bl = binders; ty = type_cstr; ":=";
+      | "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
         { let ty,c1 = match ty, c1 with
           | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
@@ -353,7 +353,7 @@ GRAMMAR EXTEND Gram
       | "cofix" -> { false } ] ]
   ;
   fix_decl:
-    [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":=";
+    [ [ id=identref; bl=binders_fixannot; ty=let_type_cstr; ":=";
         c=operconstr LEVEL "200" ->
           { (id,fst bl,snd bl,c,ty) } ] ]
   ;
@@ -525,7 +525,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
 
-  type_cstr:
+  let_type_cstr:
     [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ]
   ;
   END
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index efcb2635be..1387ca4675 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -418,19 +418,19 @@ GRAMMAR EXTEND Gram
   rec_definition:
     [ [ id_decl = ident_decl;
 	bl = binders_fixannot;
-        rtype = type_cstr;
+        rtype = rec_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 = type_cstr;
+    [ [ id_decl = ident_decl; binders = binders; rtype = rec_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}
         } ]]
   ;
-  type_cstr:
+  rec_type_cstr:
     [ [ ":"; c=lconstr -> { c }
       | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ]
   ;