diff options
| author | Théo Zimmermann | 2020-03-16 19:10:47 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-16 19:10:47 +0100 |
| commit | 901cbfab468efa868e3838c2009ac09978ee661a (patch) | |
| tree | 869ad3fbaabbcccb8fc2b8c1a9a83585246887fe /kernel/indtypes.ml | |
| parent | d967862488cb10448bf063b7c272929bfb7f8412 (diff) | |
| parent | 306a9dd33cc0f18e86f159c180ecd826f56f24db (diff) | |
Merge PR #11813: Fixed link to "match" syntax figures.
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions