From df313cefbaddb57f89650171e59e3abcb168a273 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 May 2013 22:47:35 +0000
Subject: Now printing body of abbreviations (i.e. notation with a name) with
 full usage of notations instead of the previous cheap way to prevent
 circularity in printing by deactivating all notations.

(Since "->" became a notation, printing abbreviations without
notations at all had become even more inconvenient).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/prettyp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ee6a5e18da..bc9137edea 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -439,7 +439,9 @@ let gallina_print_syntactic_def kn =
        (str "Notation " ++ pr_qualid qid ++
         prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
         spc () ++ str ":=") ++
-     spc () ++ Constrextern.without_symbols pr_glob_constr c)
+     spc () ++
+     Constrextern.without_specific_symbols
+       [Notation.SynDefRule kn] pr_glob_constr c)
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
-- 
cgit v1.2.3