diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 13:14:09 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 13:14:09 +0200 |
commit | 73fd3afba9e8917dfc0644d1d8d9b22063cfa2fe (patch) | |
tree | 408d331e0a41d21fa2a787c54504e112962f195a /plugins/ltac/rewrite.ml | |
parent | 77e4a3712dff87e5941dd93ebfa8028039ab0715 (diff) | |
parent | 5e7d5491304ce3765fa245bb697a239b05921636 (diff) |
Merge PR#698: Trunk misc
Diffstat (limited to 'plugins/ltac/rewrite.ml')
0 files changed, 0 insertions, 0 deletions