From 8f72678f7a1fc1d0e2c9ac7a5f682ce100bfa403 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 11 Jun 2009 18:59:06 +0000
Subject: 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
---
 toplevel/cerrors.ml | 4 ++--
 toplevel/himsg.ml   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 4250040ec4..f9a3364301 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 ())
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4e5eded8e4..e8a8dcb7c7 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -525,7 +525,7 @@ let pr_constraints printenv env evm =
       pr_evar_defs evm
       
 let explain_unsatisfiable_constraints env evd constr =
-  let evm =  evd in
+  let evm = Evarutil.nf_evars evd in
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++
-- 
cgit v1.2.3