diff options
| author | Emilio Jesus Gallego Arias | 2019-06-25 03:40:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-02 16:12:16 +0200 |
| commit | 8db5fed73ce71dd7c469d5633682dddd8148b65a (patch) | |
| tree | 665453fcf3cbcdf7658da3391625044368c2ebef /vernac | |
| parent | 20254d7fa38c99608042a878ec0c2975f9887ce6 (diff) | |
[declare] Cleanup on imports, move exception.
We cleanup a few imports on Declare, and indeed we find a suspicious
exception `AlreadyDeclared` present in `CErrors` where it should not
be there.
We move it to `Declare`, waiting for more investigation.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 2 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 5 |
2 files changed, 3 insertions, 4 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 5c5a4ffbcb..ba1191285a 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -85,8 +85,6 @@ let vernac_interp_error_handler = function str "Tactic failure" ++ (if Pp.ismt s then s else str ": " ++ s) ++ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")." - | AlreadyDeclared msg -> - msg ++ str "." | _ -> raise CErrors.Unhandled diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 0ee15bde6e..d9b839e857 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -159,8 +159,9 @@ let try_declare_scheme what f internal names kn = | UndefinedCst s -> alarm what internal (strbrk "Required constant " ++ str s ++ str " undefined.") - | AlreadyDeclared msg -> - alarm what internal (msg ++ str ".") + | AlreadyDeclared (kind, id) as exn -> + let msg = CErrors.print exn in + alarm what internal msg | DecidabilityMutualNotSupported -> alarm what internal (str "Decidability lemma for mutual inductive types not supported.") |