diff options
author | 2013-11-02 15:37:58 +0000 | |
---|---|---|
committer | 2013-11-02 15:37:58 +0000 | |
commit | 8bec4e3fac58fd96c876a22634e5b25a566e9ce1 (patch) | |
tree | 2d6b87d46d1dc5d1631186ee28e5a2c1aefc1c37 /bootstrap/Monads.v | |
parent | bbe58bc0b1dc9e8ae44a151dfcfa3923a391ce2d (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.v | 6 |
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. |