aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--coq/ex/test-cases/change-ancestor/.cvsignore2
-rw-r--r--doc/ProofGeneral.texi2
2 files changed, 3 insertions, 1 deletions
diff --git a/coq/ex/test-cases/change-ancestor/.cvsignore b/coq/ex/test-cases/change-ancestor/.cvsignore
new file mode 100644
index 00000000..e940bcb4
--- /dev/null
+++ b/coq/ex/test-cases/change-ancestor/.cvsignore
@@ -0,0 +1,2 @@
+*.glob
+*.vo
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 1d0f156b..177601ff 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3145,7 +3145,7 @@ dependencies.
@item Mark proof commands that introduce or instantiate a
given existential variable.
@item Snapshots of proof trees for reference when you retract
-your proof to try an different approach.
+your proof to try a different approach.
@end itemize
For a more elaborated description please consult the help dialog