From ff3bc8b7c911ff19e9335995428351f6c38494e9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Nov 2005 16:16:49 +0000 Subject: [PATCH] More informative error messages. --- helm/ocaml/cic_unification/cicRefine.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 681ed4929..21bf07278 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -392,12 +392,13 @@ and type_of_aux' metasenv context t ugraph = let search = CoercGraph.look_for_coercion in let boh = search coercion_src coercion_tgt in (match boh with - | CoercGraph.NoCoercion -> - raise (RefineFailure (lazy "no coercion")) + | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> - raise (RefineFailure (lazy "not a sort in PI")) + raise + (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) | CoercGraph.NotMetaClosed -> - raise (Uncertain (lazy "Coercions on metas 1")) + raise + (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) | CoercGraph.SomeCoercion c -> Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) in -- 2.39.2