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. --- vernac/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/ppvernac.ml') diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 7e67e12cb..7aff758e9 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -102,7 +102,7 @@ open Pputils | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" - let pr_constr_as_binder_kind = function + let pr_constr_as_binder_kind = let open Notation_term in function | AsIdent -> keyword "as ident" | AsIdentOrPattern -> keyword "as pattern" | AsStrictPattern -> keyword "as strict pattern" -- cgit v1.2.3