diff options
| author | Hugo Herbelin | 2015-07-27 11:03:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-27 14:20:44 +0200 |
| commit | 9b690c608c2a48b26a8ac94325fe0008d438fb3b (patch) | |
| tree | f4d1c6619cd5d2687b2213dbfc340fec1119f3e7 | |
| parent | cb6c3ec2e66e3019cb9ee881b1e222e6e3691463 (diff) | |
Improving over 26aa224293 in reporting unexpected error during scheme creation.
This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
| -rw-r--r-- | toplevel/indschemes.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index f8f062dad6..286d164c42 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -184,9 +184,8 @@ let try_declare_scheme what f internal names kn = alarm what internal (str "Decidability lemma for mutual inductive types not supported.") | e when Errors.noncritical e -> - alarm what internal - (str "Unknown exception during scheme creation: "++ - str (Printexc.to_string e)) + alarm what internal + (str "Unexpected error during scheme creation: " ++ Errors.print e) let beq_scheme_msg mind = let mib = Global.lookup_mind mind in |