aboutsummaryrefslogtreecommitdiff
path: root/doc/tutorial/Tutorial.tex
diff options
context:
space:
mode:
authorHugo Herbelin2016-04-27 22:13:03 +0200
committerHugo Herbelin2016-04-27 22:13:03 +0200
commit74223731f771f01f71aad219056abc7dd9133631 (patch)
tree98b8a9a6b131d3727f763b1441d73b2f98be4d3e /doc/tutorial/Tutorial.tex
parent1965c3e4a1f3ab4ab8a777fe3707e71891bac162 (diff)
Revert "Protect printing of ltac's "context [...]" from possible collision"
This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd.
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
0 files changed, 0 insertions, 0 deletions