diff options
| author | Pierre-Marie Pédrot | 2016-03-07 21:35:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-07 21:43:05 +0100 |
| commit | d34a2ff176c75ea404f7eb638b6eea3ca07ab978 (patch) | |
| tree | e91e3dc750866c26099d350c2138546cf9df4b6d | |
| parent | 2f41c0280685615aae03efcdfd1d39941e7c1232 (diff) | |
Adding backtraces to scheme error messages.
| -rw-r--r-- | toplevel/indschemes.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index c4ac0e4112..aa2362ae5f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -150,12 +150,14 @@ let alarm what internal msg = | InternalTacticRequest -> (if debug then msg_warning - (hov 0 msg ++ fnl () ++ what ++ str " not defined.")) - | _ -> errorlabstrm "" msg + (hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None + | _ -> Some msg let try_declare_scheme what f internal names kn = try f internal names kn - with + with e -> + let e = Errors.push e in + let msg = match fst e with | ParameterWithoutEquality cst -> alarm what internal (str "Boolean equality not found for parameter " ++ pr_con cst ++ @@ -186,6 +188,11 @@ let try_declare_scheme what f internal names kn = | e when Errors.noncritical e -> alarm what internal (str "Unexpected error during scheme creation: " ++ Errors.print e) + | _ -> iraise e + in + match msg with + | None -> () + | Some msg -> iraise (UserError ("", msg), snd e) let beq_scheme_msg mind = let mib = Global.lookup_mind mind in |