diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -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 = |