diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-30 20:45:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-30 20:45:20 +0200 |
| commit | fa69f12babe7f04fbda9a22eaf76736a96f0fdea (patch) | |
| tree | cc6250719586805f0c58cacb854bf81a376ec62f /pretyping/evd.ml | |
| parent | 26c8ce24a5dad0d54c6efbc7265a15f8d92dfb0b (diff) | |
Clarifying 'No such bound variable' message in apply, as suggested in #2387
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 481e4275a..b2bad0c0b 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1342,6 +1342,20 @@ let meta_reassign mv (v, pb) evd = let meta_name evd mv = try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous +let explain_no_such_bound_variable evd id = + let mvl = + List.rev (Metamap.fold (fun n clb l -> + let na = fst (clb_name clb) in + if na != Anonymous then out_name na :: l else l) + evd.metas []) in + errorlabstrm "Evd.meta_with_name" + (str"No such bound variable " ++ pr_id id ++ + (if mvl == [] then str " (no bound variables at all in the expression)." + else + (str" (possible name" ++ + str (if List.length mvl == 1 then " is: " else "s are: ") ++ + pr_enum pr_id mvl ++ str")."))) + let meta_with_name evd id = let na = Name id in let (mvl,mvnodef) = @@ -1353,8 +1367,7 @@ let meta_with_name evd id = evd.metas ([],[]) in match mvnodef, mvl with | _,[] -> - errorlabstrm "Evd.meta_with_name" - (str"No such bound variable " ++ pr_id id ++ str".") + explain_no_such_bound_variable evd id | ([n],_|_,[n]) -> n | _ -> |