From a508078b3985ad932ac6cf24455d7360b6ab594e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 3 May 2012 19:26:39 +0000 Subject: [PATCH] Speed up: moved a #ppterm inside the lazy it belongs to. --- matita/components/ng_refiner/nCicRefiner.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml index 563fe3928..550c75e93 100644 --- a/matita/components/ng_refiner/nCicRefiner.ml +++ b/matita/components/ng_refiner/nCicRefiner.ml @@ -505,13 +505,14 @@ and try_coercions status (* we try with a coercion *) let rec first exc = function | [] -> - let expty = - match expty with - `Type expty -> status#ppterm ~metasenv ~subst ~context expty - | `Sort -> "[[sort]]" - | `Prod -> "[[prod]]" in pp (lazy "WWW: no more coercions!"); - raise (wrap_exc (lazy (localise orig_t, Printf.sprintf + raise (wrap_exc (lazy + let expty = + match expty with + `Type expty -> status#ppterm ~metasenv ~subst ~context expty + | `Sort -> "[[sort]]" + | `Prod -> "[[prod]]" in + (localise orig_t, Printf.sprintf "The term\n%s\nhas type\n%s\nbut is here used with type\n%s" (status#ppterm ~metasenv ~subst ~context t) (status#ppterm ~metasenv ~subst ~context infty) -- 2.39.2