diff options
author | 2018-07-02 15:06:17 +0200 | |
---|---|---|
committer | 2018-07-02 15:06:17 +0200 | |
commit | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (patch) | |
tree | 1d1c7c47fff5688105d0f868f9ab89d479ede899 /plugins/setoid_ring | |
parent | f6f606232ae3c32e5c90d4fd427721875529b777 (diff) | |
parent | 47bbe39d480f02dc92e4856fa8d872f52b9903a4 (diff) |
Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points of Camlp5
Diffstat (limited to 'plugins/setoid_ring')
0 files changed, 0 insertions, 0 deletions