diff options
| author | Pierre-Marie Pédrot | 2021-03-29 12:06:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-29 12:18:12 +0200 |
| commit | adc223385c7aa8b43761f4ebb102b4b7b1241123 (patch) | |
| tree | 215dd82423b75fa63b51822867770976906704be /kernel/genOpcodeFiles.ml | |
| parent | e414d25f120696dbd1956b230801d22810746f58 (diff) | |
Print type of offending expression in Ltac2 not-unit warning.
Partial fix of #14013.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions