diff options
| author | Emilio Jesus Gallego Arias | 2020-03-30 15:02:50 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:38 -0400 |
| commit | 1320d5004b58f33c2274bfdc0629d7f513cd49c4 (patch) | |
| tree | ed27831377ff2a36be3011fbb4158ed0f2c69288 /vernac/comDefinition.ml | |
| parent | b2b325a1d3c143f90a50a61cc9410efcd437d4b0 (diff) | |
[declare] [nit] Get `fix_exn` only in the case of an exception.
Suggested by Gaëtan Gilbert.
Diffstat (limited to 'vernac/comDefinition.ml')
0 files changed, 0 insertions, 0 deletions