From 4a69c594b484cb7e9af28b8ba9608a228e2376f1 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Thu, 16 May 2019 11:00:05 -0400
Subject: [refman] Fix up the grammar entry for field_def

---
 doc/sphinx/language/gallina-extensions.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 96e74bf118..5e214f6f7f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor
 
   .. productionlist::
     record_term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : name [binders] := `record_term`
+    field_def : `ident` [`binders`] := `term`
 
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
-- 
cgit v1.2.3