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 | |
| parent | b2b325a1d3c143f90a50a61cc9410efcd437d4b0 (diff) | |
[declare] [nit] Get `fix_exn` only in the case of an exception.
Suggested by Gaëtan Gilbert.
| -rw-r--r-- | vernac/declareDef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 356e8f091e..1607771598 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -60,10 +60,10 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = dref let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = - let fix_exn = Declare.Internal.get_fix_exn entry in try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry with exn -> let exn = Exninfo.capture exn in + let fix_exn = Declare.Internal.get_fix_exn entry in Exninfo.iraise (fix_exn exn) let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = |