diff options
author | 2017-10-10 15:54:38 +0200 | |
---|---|---|
committer | 2017-10-10 15:54:38 +0200 | |
commit | f790c6ac8b16f71aae4868cbcad87a39f50727e3 (patch) | |
tree | 026665b355bf3c2712c3148b8e459e85ee10199a /plugins/ltac/tactic_matching.mli | |
parent | 16f169b3c756aa3c5cbc38eb13412ba23ae2937d (diff) | |
parent | 1d8725b59309c2c9f870eb52a2daebe87ed9ad5b (diff) |
Merge PR #540: [configure] Support for flambda flags.
Diffstat (limited to 'plugins/ltac/tactic_matching.mli')
0 files changed, 0 insertions, 0 deletions