From 36c2559cefb54dc503fea375d15d3224992f6221 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 13 Nov 2014 20:28:54 +0100 Subject: Slightly improving error messages when mismatch with Proof using at Qed time. --- kernel/term_typing.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 79b3d518a..5c95aacae 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -196,9 +196,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in if not (Id.Set.subset inferred_set declared_set) then - error ("The following section variable are used but not declared:\n"^ - (String.concat ", " (List.map Id.to_string - (Id.Set.elements (Idset.diff inferred_set declared_set))))) in + let l = Id.Set.elements (Idset.diff inferred_set declared_set) in + let n = List.length l in + errorlabstrm "" (Pp.(str "The following section " ++ + str (String.plural n "variable") ++ + str " " ++ str (String.conjugate_verb_to_be n) ++ + str " used but not declared:" ++ + fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map pi1 (named_context env) in -- cgit v1.2.3