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