aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-21 22:24:59 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-21 22:24:59 +0100
commiteb91ccaf236bc9a60a1e216b76a0a42980c072a7 (patch)
tree0bc32293ac19ddd63cf764ccbd224b086c7836bc /grammar
parentb75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff)
parent0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (diff)
Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.
Diffstat (limited to 'grammar')
0 files changed, 0 insertions, 0 deletions