3 files changed, 4 insertions, 4 deletions
diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css
index 0b1e640b38..d1b2ce1112 100644
--- a/doc/common/styles/html/simple/style.css
+++ b/doc/common/styles/html/simple/style.css
@@ -10,4 +10,4 @@
     margin: 0pt;
     padding: .5ex 1em;
     list-style: none 
-}
-\ No newline at end of file
+}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 574591185c..5fb4585884 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -547,7 +547,7 @@ Yet another way of branching without backtracking is the following structure:
 $v_2$ which must be tactic values. The tactic value $v_1$ is applied in each
 subgoal independently and if it fails \emph{to progress} then $v_2$ is
 applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt
-  first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress}
+  first [} {\tt progress} {\tacexpr}$_1$ {\tt |}
   {\tacexpr}$_2$ {\tt ]} (except that if it fails, it fails like
 $v_2$). Branching is left-associative.
 
@@ -561,7 +561,7 @@ The tactic
 is a generalization of the biased-branching tactics above. The
 expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied
 to each subgoal independently. For each goal where $v_1$ succeeds at
-least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied
+least once, {\tacexpr}$_2$ is evaluated to $v_2$ which is then applied
 collectively to the generated subgoals. The $v_2$ tactic can trigger
 backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt
   tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
diff --git a/doc/refman/index.html b/doc/refman/index.html
index 9b5250abcb..b937350e6e 100644
--- a/doc/refman/index.html
+++ b/doc/refman/index.html
@@ -11,4 +11,4 @@
   <FRAME SRC="menu.html">
 </FRAMESET>
 
-</HTML>
-\ No newline at end of file
+</HTML>