From 59c1da7b30cc49916a636682556ed1b9532cd146 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Jul 2008 19:05:27 +0000 Subject: [PATCH] Error message improved. --- helm/software/components/content_pres/termContentPres.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 3ee9e7fe9..bffd18976 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -319,7 +319,11 @@ let instantiate21 idrefs env l1 = assert (CicNotationEnv.well_typed ty value); (* INVARIANT *) (* following assertion should be a conditional that makes this * instantiation fail *) - assert (CicNotationEnv.well_typed expected_ty value); + if not (CicNotationEnv.well_typed expected_ty value) then + begin + prerr_endline ("The variable " ^ name ^ " is used with the wrong type in the notation declaration"); + assert false + end; let value = CicNotationEnv.term_of_value value in let value = match expected_ty with -- 2.39.5