diff options
| author | Emilio Jesus Gallego Arias | 2020-04-21 13:45:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 18:05:14 +0200 |
| commit | ad84e6948a86db491a00bb92ec3e00a9a743b1f9 (patch) | |
| tree | 7a85b4dfe31bfc26b97baaa6acd306e9ff144bb8 /vernac/declareDef.ml | |
| parent | e4bfbdfc4b4944d6e6d702eb732bce24f962e67f (diff) | |
[declare] Remove fix_exn internal access.
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1809c2bc91..90d88b95a2 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -59,13 +59,6 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; dref -let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = - 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 = match possible_indexes with | Some possible_indexes -> |