diff options
| author | Paolo G. Giarrusso | 2020-05-25 11:43:09 +0200 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2020-05-25 11:43:09 +0200 |
| commit | 0df0e9cc7d5db550136c1b4d31834cd8e1d8633e (patch) | |
| tree | de2c634016b88e409b0717062b8f3446d0c81396 /dev/include | |
| parent | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (diff) | |
Fix #12406: fix Coq type error in dependent induction's Ltac
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions