aboutsummaryrefslogtreecommitdiffhomepage
path: root/man
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-16 19:58:13 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-16 20:17:20 +0200
commit2a3a190384cedc4dfdea5bdf1079d903db624cb8 (patch)
tree79af95a7dd4c7ecf822ea850f379652846167a30 /man
parent682aa67cc808e1d46b35f6f9c848946cabc226f7 (diff)
Better printing of Ltac values.
Diffstat (limited to 'man')
0 files changed, 0 insertions, 0 deletions