diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-28 07:33:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-28 07:33:37 +0000 |
| commit | c43f9128237ac16fa0d7741744e3944ca72e7475 (patch) | |
| tree | 9d36fa1cb3364d16c00e506d786822303b6a027c /toplevel/himsg.ml | |
| parent | 87bd13c7a6552f33782e0e69ef705b356a2cf741 (diff) | |
More informative error when a global reference is used in a context of
local variables which is a different from the one of its definition. E.g.:
Section A.
Variable n:nat.
Definition c:=n.
Goal True.
clear n.
Check c.
[I'm however unsure that "n" should not continue to be accessible via
some global (qualified) name, even after the "clear n".]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16256 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index cc05f371e..61830603b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -60,10 +60,11 @@ let explain_bad_assumption env j = brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++ str "because this term is not a type." -let explain_reference_variables c = - let pc = pr_lconstr c in - str "The constant" ++ spc () ++ pc ++ spc () ++ - str "refers to variables which are not in the context." +let explain_reference_variables id c = + (* c is intended to be a global reference *) + let pc = pr_global (Globnames.global_of_constr c) in + pc ++ strbrk " depends on the variable " ++ pr_id id ++ + strbrk " which is not declared in the context." let rec pr_disjunction pr = function | [a] -> pr a @@ -528,8 +529,8 @@ let explain_type_error env sigma err = explain_not_type env sigma j | BadAssumption c -> explain_bad_assumption env c - | ReferenceVariables id -> - explain_reference_variables id + | ReferenceVariables (id,c) -> + explain_reference_variables id c | ElimArity (ind, aritylst, c, pj, okinds) -> explain_elim_arity env ind aritylst c pj okinds | CaseNotInductive cj -> |