diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-16 08:46:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-16 08:46:27 +0000 |
| commit | b33c18ba8edc25c7f4b0be62db4e845dc8693a2f (patch) | |
| tree | 4953c33fc33986555e3b9b5a6f3a84df585bd32f | |
| parent | 2556a4bcfe9bbad8b3fe555997bb272102fec1dd (diff) | |
Fixing beautification of "thm_token" (missing space) + improvements.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14654 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 b1ba16b5c..849f67fe6 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 aac6f3e0e..ccfeb3dba 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'"' |