diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-10 14:50:13 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-10 16:38:17 +0100 |
commit | 2bad1e8d896b40495bc8579e407f142f7f3fb7d9 (patch) | |
tree | 0fee1c7082449ec26a98e0b2b0a7b699453273ca /library | |
parent | b382bb1b42319d7be422f92fd196df8bfbe21a83 (diff) | |
parent | ab1d8792143a05370a1efe3d19469c25b82d7097 (diff) |
Merge origin/v8.5 into trunk
Did some manual merge in tactics/tactics.ml.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions