diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-11 18:59:06 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-11 18:59:06 +0000 |
| commit | 8f72678f7a1fc1d0e2c9ac7a5f682ce100bfa403 (patch) | |
| tree | 4aa74c5721a3b24372cfa0d72784749de204d493 /toplevel/cerrors.ml | |
| parent | 80105c8482bd487782dcab8161fa1fc1f3fdf635 (diff) | |
Use a lazy value for the message in FailError, so that it won't be
unnecessarily computed when the user won't see it (avoids the costly
nf_evar_defs in typeclass errors).
Add hook support for mutual definitions in Program.
Try to solve only the argument typeclasses when calling [refine].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/cerrors.ml')
| -rw-r--r-- | toplevel/cerrors.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 4250040ec..f9a336430 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -85,7 +85,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) | RecursionSchemeError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) - | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when s <> mt () -> + | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> explain_exn_default_aux anomaly_string report_fn exc | Proof_type.LtacLocated (s,exc) -> hov 0 (Himsg.explain_ltac_call_trace s ++ fnl () @@ -108,7 +108,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> hov 0 (str "Error: Tactic failure" ++ - (if s <> mt() then str ":" ++ s else mt ()) ++ + (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ if i=0 then str "." else str " (level " ++ int i ++ str").") | Stdpp.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) |