aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-14 15:03:48 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-16 17:10:16 +0200
commitf29a9c409272271260256792f64abf7475984e77 (patch)
tree0b45039fdd111b678d362c1e5414a6b2d550f4e8 /vernac/classes.ml
parentd74d72419f5e9b68fe8ec9e8c046faecacf9f2f4 (diff)
[sphinx] Improve rewrite section in tactic chapter.
Including a fix to the example given in #7407.
Diffstat (limited to 'vernac/classes.ml')
0 files changed, 0 insertions, 0 deletions