diff options
| author | Théo Zimmermann | 2018-07-28 19:36:54 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-28 19:36:54 +0200 |
| commit | f416349d504dcdd3a5744c85ab4554f2f6989ebf (patch) | |
| tree | 9a4efb346763a70863d07085b28f30ee48e315fd /lib/pp_diff.ml | |
| parent | 3c41245404eacd105c0dbcae78f47ba103131788 (diff) | |
| parent | 6f52f7bce0de9ac58142b05e17b5dc380fc169e7 (diff) | |
Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to unify" message
Diffstat (limited to 'lib/pp_diff.ml')
0 files changed, 0 insertions, 0 deletions