aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-07 11:23:41 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-07 11:23:41 +0200
commit77e4a3712dff87e5941dd93ebfa8028039ab0715 (patch)
treeca9db76e334d40fb19938b014a20c3691866092a /grammar
parent3e29266b1e2dfb970ca77fb5910b6a5860d4ad1a (diff)
parent48476a32fa9221b216074695cceeaa0b34fc659b (diff)
Merge PR#717: [proof] Deprecate "proof mode" API
Diffstat (limited to 'grammar')
0 files changed, 0 insertions, 0 deletions