diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-08-18 20:25:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-08-18 20:25:14 +0200 |
| commit | fa141fa1d2df2720f84a3e2c1fc4900a47f9939f (patch) | |
| tree | 63d15d161d826892cf6c8b5289284d02a28cc3ee /pretyping/redops.mli | |
| parent | 03932df7e8ddaa9f80be0be4073176521b8ddea3 (diff) | |
| parent | 02bcddbba985b65ac167f63b48bf2bd5bceffa1f (diff) | |
Merge remote-tracking branch 'github/bug4978' into v8.6
Diffstat (limited to 'pretyping/redops.mli')
0 files changed, 0 insertions, 0 deletions