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.

---
 interp/interp.mllib | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/interp.mllib')

diff --git a/interp/interp.mllib b/interp/interp.mllib
index 7f14fe42b4..c9a0315267 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,5 @@
+Stdarg
+Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
@@ -16,5 +18,3 @@ Constrextern
 Coqlib
 Discharge
 Declare
-Stdarg
-Constrarg
-- 
cgit v1.2.3