diff options
| author | coqbot-app[bot] | 2021-04-08 12:27:44 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-08 12:27:44 +0000 |
| commit | b7e2dfcc1918e028fb8a4fe353f929f104f13b77 (patch) | |
| tree | 0d11c44e1df6576901e466f1212d1f2ff2e4bdcd /dev/header.ml | |
| parent | 2b8d8b996b7ae9b5c170792cbf45c4fd96ed3658 (diff) | |
| parent | adc223385c7aa8b43761f4ebb102b4b7b1241123 (diff) | |
Merge PR #14027: Print type of offending expression in Ltac2 not-unit warning.
Reviewed-by: JasonGross
Diffstat (limited to 'dev/header.ml')
0 files changed, 0 insertions, 0 deletions