aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-11-13 20:28:54 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-11-19 18:52:13 +0100
commit36c2559cefb54dc503fea375d15d3224992f6221 (patch)
treee2ddfb03636963985b80b6fad97d736679c81d6e
parent090fffa57b2235f70d4355f5dc85d73fa2634655 (diff)
Slightly improving error messages when mismatch with Proof using at Qed time.
-rw-r--r--kernel/term_typing.ml10
1 files 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