diff options
| author | Pierre-Marie Pédrot | 2020-11-17 19:06:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-17 19:06:34 +0100 |
| commit | 7c79a0da543536da48cd49cb9b09682fb9a6efe8 (patch) | |
| tree | f7b6a3c08b0c86ced67793bb9e600bd254f3096a /kernel/indTyping.ml | |
| parent | f1b7a377473919327a270090090d774b678f6628 (diff) | |
| parent | 05cf3fca1d0800e4cefaed3cb1825a8420ce9f2c (diff) | |
Merge PR #13397: Adding heterogeneous map on named contexts.
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/indTyping.ml')
0 files changed, 0 insertions, 0 deletions