aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-24 02:37:26 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-24 02:37:26 +0200
commit28f8da9489463b166391416de86420c15976522f (patch)
tree5456aa680f6e54f7f7bf71f5c4d99dc4e8709e03 /grammar
parent05add9c71214bebf86f1892c5ad946cdce19009a (diff)
parentc1e9a27d383688e44ba34ada24fe08151cb5846e (diff)
Merge PR#642: Small cleanup on `close_proof` type.
Diffstat (limited to 'grammar')
0 files changed, 0 insertions, 0 deletions