diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 4 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
2 files changed, 3 insertions, 3 deletions
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() ++ |