aboutsummaryrefslogtreecommitdiffhomepage
path: root/bootstrap/Monads.v
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:37:58 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:37:58 +0000
commit8bec4e3fac58fd96c876a22634e5b25a566e9ce1 (patch)
tree2d6b87d46d1dc5d1631186ee28e5a2c1aefc1c37 /bootstrap/Monads.v
parentbbe58bc0b1dc9e8ae44a151dfcfa3923a391ce2d (diff)
Typos in a comment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16997 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'bootstrap/Monads.v')
-rw-r--r--bootstrap/Monads.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index bff4e5e5f..f3f2eb653 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -412,9 +412,9 @@ Module Logic.
"search" implementations (including Tac interactive prover's
tactics). Yet it's quite hard to wrap your head around these. I
recommand reading a few times the "Backtracking, Interleaving, and
- Terminating Monad Transformers" paper by O. Kiselyov, C. Chen,
- D. Fridman. The peculiar shape of the monadic type is reminiscent
- of that of the continuation monad transformer.
+ Terminating Monad Transformers" paper by O. Kiselyov, C. Shan,
+ D. Friedman, and A. Sabry. The peculiar shape of the monadic type
+ is reminiscent of that of the continuation monad transformer.
The paper also contains the rational for the [split] abstraction.