diff options
| author | coqbot-app[bot] | 2020-10-01 16:04:16 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-01 16:04:16 +0000 |
| commit | 7ffb5e663784fffb2cd6aae87bc38a5dc2f37710 (patch) | |
| tree | d92f9d7972f7eed790d5eef42a143105b05e6239 /dev/doc | |
| parent | 1c919ed6fa476f0f7a16d69e58989f3d75104910 (diff) | |
| parent | afe7005394721b81d32ab5300325c341f99473cf (diff) | |
Merge PR #13123: Fix combining uniform parameters and mutual inductives.
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions