aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib3
-rw-r--r--dev/top_printers.ml3
2 files changed, 4 insertions, 2 deletions
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