diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-06-03 13:39:46 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-03 13:39:46 +0200 |
commit | 9d60ddc84e95a030913fc4b3db705f3ec894fdb2 (patch) | |
tree | 2b5160a744fa279401dc1229ae3106aee59bd49b /parsing/g_tactic.ml4 | |
parent | 9f3be24242f5397886875b51eaee7392a4aba473 (diff) | |
parent | aa99eef44dfa439a7c62b29f1a6c39525dc82acf (diff) |
Merge remote-tracking branch 'github/pr/159' into trunk
Diffstat (limited to 'parsing/g_tactic.ml4')
0 files changed, 0 insertions, 0 deletions