diff options
| author | Michael Soegtrop | 2020-07-05 07:49:37 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2020-07-05 07:49:37 +0200 |
| commit | 0545c9402310efe0656793197c996d04d554ecb8 (patch) | |
| tree | a7ee9471b02a4cad3f87a241299decb36bc935f7 /lib/objFile.ml | |
| parent | 99889823890c9d414335dc25df8f30ae06575f94 (diff) | |
| parent | 810197a6577c7a4a40f406ae64f918f72e7d0012 (diff) | |
Merge PR #12594: Fix ltac2 type parameters
Reviewed-by: MSoegtropIMC
Reviewed-by: gares
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions