From 51efb80ac1699a27e0003349bb766a430fbaf86a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:09:20 +0000
Subject: Split Egrammar into Egramml and Egramcoq

 Two gains:
 - no Summary in Grammar.cma
 - get rid of the hack concerning error_invalid_pattern_notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/printers.mllib  | 3 ++-
 dev/top_printers.ml | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 545a1881fa..928bfc4940 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -139,7 +139,8 @@ Printer
 Pptactic
 Ppdecl_proof
 Tactic_printer
-Egrammar
+Egramml
+Egramcoq
 Himsg
 Cerrors
 Locality
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4fd6171ac8..2a2833caa5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -411,7 +411,8 @@ END
 
 open Pcoq
 open Genarg
-open Egrammar
+open Egramml
+open Egramcoq
 
 let _ =
   try
-- 
cgit v1.2.3