From 5fb1677a4bf62155ef0f57c0a0b189d42e05505f Mon Sep 17 00:00:00 2001
From: Sam Pablo Kuper
Date: Fri, 19 Oct 2018 04:45:33 +0100
Subject: Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"

---
 doc/sphinx/credits.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index ffdc4f3ec6..57f1174d59 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -120,7 +120,7 @@ G. Dowek, allowed hierarchical developments of mathematical theories.
 This high-level language was called the *Mathematical Vernacular*.
 Furthermore, an interactive *Theorem Prover* permitted the incremental
 construction of proof trees in a top-down manner, subgoaling recursively
-and backtracking from dead-alleys. The theorem prover executed tactics
+and backtracking from dead-ends. The theorem prover executed tactics
 written in CAML, in the LCF fashion. A basic set of tactics was
 predefined, which the user could extend by his own specific tactics.
 This system (Version 4.10) was released in 1989. Then, the system was
-- 
cgit v1.2.3