From 1c5e311d6a92deb66ba412c56516a4b71a513e01 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 15:35:05 +0100 Subject: Fixing printing of "only parsing" in abbreviations. --- printing/ppvernac.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3494ad006..be1587918 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1015,7 +1015,10 @@ module Make (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match compat with None -> [] | Some v -> [SetCompatVersion v])) + (match compat with + | None -> [] + | Some Flags.Current -> [SetOnlyParsing] + | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( -- cgit v1.2.3 From 00f1839a2cee1cb1fa4dc207391c4a5bb588f71a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 15:40:40 +0100 Subject: Fixing space in printing several list of implicit arguments. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index be1587918..75271e21e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1060,7 +1060,7 @@ module Make in print_arguments nargs args ++ if not (List.is_empty more_implicits) then - str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits + prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function -- cgit v1.2.3 From edb7a97487cb5e38bb284472eacfd1b58fa97f84 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Nov 2016 07:00:31 +0100 Subject: Fixing space in printing "Context". --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 75271e21e..953383321 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -913,7 +913,7 @@ module Make | VernacContext l -> return ( hov 1 ( - keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) + keyword "Context" ++ pr_and_type_binders_arg l) ) | VernacDeclareInstances insts -> -- cgit v1.2.3 From ab3b0de5902082f7e692901979aa8330394c2f26 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Nov 2016 12:58:02 +0100 Subject: Fixing printing of "Set Warnings Append". --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 953383321..5d6d36d56 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1131,7 +1131,7 @@ module Make | VernacSetAppendOption (na,v) -> return ( hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ str v) + spc() ++ keyword "Append" ++ spc() ++ qs v) ) | VernacAddOption (na,l) -> return ( -- cgit v1.2.3