diff options
| author | Théo Zimmermann | 2019-11-26 10:59:03 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-26 10:59:03 +0100 |
| commit | 669075119cc0ea8e495a83668fad4f6c1e4f5968 (patch) | |
| tree | 409e86ccd2f8e6d565f9a3953a64dc6af6dfb0cd /kernel/indTyping.ml | |
| parent | 0e9cd0fe99216bc09a09a0da6906f9501b682223 (diff) | |
| parent | f58291264e3b2197152bfca8879f8e0af64ce675 (diff) | |
Merge PR #11034: Update update-compat.py
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/indTyping.ml')
0 files changed, 0 insertions, 0 deletions