diff options
| -rw-r--r-- | parsing/ppvernac.ml | 4 | ||||
| -rwxr-xr-x[-rw-r--r--] | tools/beautify-archive | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b1ba16b5cf..849f67fe68 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -414,8 +414,8 @@ let pr_grammar_tactic_rule n (_,pil,t) = let pr_statement head (id,(bl,c,guard)) = assert (id<>None); - hov 0 - (head ++ pr_lident (Option.get id) ++ spc() ++ + hov 1 + (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ pr_opt (pr_guard_annot bl) guard ++ str":" ++ pr_spc_lconstr c) diff --git a/tools/beautify-archive b/tools/beautify-archive index aac6f3e0e5..ccfeb3dbaa 100644..100755 --- a/tools/beautify-archive +++ b/tools/beautify-archive @@ -47,6 +47,6 @@ for i in $vfiles; do mv -u -f $NEWARCHIVE/$i $i done echo -------- Beautification completed ------------------------------------- -echo Old files are in directory '"$OLDARCHIVE"' +echo Old files are in directory '"'$OLDARCHIVE'"' echo New files are in current directory -echo You can now remove the beautification directory '"$NEWARCHIVE"' +echo You can now remove the beautification directory '"'$NEWARCHIVE'"' |