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/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 3dfe308a5d..b29af6680d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Genarg
 open Geninterp
 open Stdarg
 open Libnames
-open Notation_term
+open Notation_gram
 open Misctypes
 open Locus
 open Decl_kinds
-- 
cgit v1.2.3