From 455d5ee36dc36cbf094ddccf43059cddceedcd1f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 22 Dec 2013 02:32:49 +0100
Subject: Notations now accept the $(...)$ tactic-in-term syntax. They are
 resolved at internalization time.

---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/printers.mllib')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 2c4f843978..1d560e6992 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -139,6 +139,7 @@ Pputils
 Stdarg
 Constrarg
 Constrexpr_ops
+Genintern
 Notation_ops
 Topconstr
 Notation
@@ -148,7 +149,6 @@ Impargs
 Syntax_def
 Implicit_quantifiers
 Smartlocate
-Genintern
 Constrintern
 Modintern
 Constrextern
-- 
cgit v1.2.3