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

(limited to 'printing/ppconstr.mli')

diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 127c4471cd..05f48ec79d 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -16,7 +16,7 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
-open Notation_term
+open Notation_gram
 
 val prec_less : precedence -> tolerability -> bool
 
-- 
cgit v1.2.3