From 5b194f6c4f16b99fe8ebe3c8004c31c01aec0b3b Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 27 Sep 2020 00:49:28 -0700
Subject: Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."

---
 doc/tools/docgram/fullGrammar    | 1 -
 doc/tools/docgram/orderedGrammar | 1 -
 2 files changed, 2 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2ee8e4347e..328175e65c 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1761,7 +1761,6 @@ int_or_id: [
 ]
 
 language: [
-| "Ocaml"      (* extraction plugin *)
 | "OCaml"      (* extraction plugin *)
 | "Haskell"      (* extraction plugin *)
 | "Scheme"      (* extraction plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index aae96fc966..6ae99880b3 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1268,7 +1268,6 @@ int_or_id: [
 ]
 
 language: [
-| "Ocaml"      (* extraction plugin *)
 | "OCaml"      (* extraction plugin *)
 | "Haskell"      (* extraction plugin *)
 | "Scheme"      (* extraction plugin *)
-- 
cgit v1.2.3