diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 03:18:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:54 -0400 |
| commit | 305ccf3523bf356c9e099f2f0c848bfba4b61e94 (patch) | |
| tree | fb011e1dfd5dce0c81bc7dccb7706ee757107d1d | |
| parent | e3a9da879d9c0c78bff44fec2cdfc9f111a9e03c (diff) | |
[vernac] Make local exception local
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f935cea534..151e675e8c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1603,12 +1603,11 @@ let get_nth_goal ~pstate n = let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl -exception NoHyp - (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = + let exception NoHyp in let open Context.Named.Declaration in try (* Fallback early to globals *) |