aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-04-27 09:57:09 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-04-27 10:00:36 +0200
commitfa27856d2d4ac0f55b99b9406b74301057deb0aa (patch)
tree3369e1a7fdc21eb8eb7e1f086d8cdef2fae10735 /printing/ppvernac.ml
parentadc2035410a339cfa88dae527b631f5131adaa54 (diff)
contracting the type of "Pfedit.solve_by_implicit_tactic"
Diffstat (limited to 'printing/ppvernac.ml')
0 files changed, 0 insertions, 0 deletions