diff options
| author | herbelin | 2013-05-05 22:47:35 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-05 22:47:35 +0000 |
| commit | df313cefbaddb57f89650171e59e3abcb168a273 (patch) | |
| tree | d454b60baf938da9a3c2a59e70fc474750057b0f /printing/prettyp.ml | |
| parent | 9b67b88dc13cbd0720cf88e105a60732f8ab619b (diff) | |
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
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 " : " |