From 63b530234e0b19323a50c52434a7439518565c81 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 24 May 2018 03:15:17 +0200
Subject: [notations] Split interpretation and parsing of notations

Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.

We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
---
 plugins/ltac/extraargs.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/extraargs.ml4')

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 702b830342..4e7c8b754f 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -251,7 +251,7 @@ END
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
-- 
cgit v1.2.3