From d8dc892dc4e50462163053124c9bafcd312433a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Oct 2019 22:07:00 +0200
Subject: Notations: Avoiding computing parsing rule when in onlyprinting mode.

In particular, this fixes #9741.
---
 parsing/notation_gram.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'parsing/notation_gram.ml')

diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 9f133ca9d4..ffc92fa53a 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -37,7 +37,4 @@ type one_notation_grammar = {
   notgram_prods : grammar_constr_prod_item list list;
 }
 
-type notation_grammar = {
-  notgram_onlyprinting : bool;
-  notgram_rules : one_notation_grammar list
-}
+type notation_grammar = one_notation_grammar list
-- 
cgit v1.2.3