diff options
| author | herbelin | 2003-12-20 10:37:37 +0000 |
|---|---|---|
| committer | herbelin | 2003-12-20 10:37:37 +0000 |
| commit | a4cea80b48134a933d1567e17b162e446c23e47d (patch) | |
| tree | 0b0215cebcbab0c7c2c7a3a3506cb1f04a1c64a4 | |
| parent | ba470631036c16912f30a2ffb2e8a43e0362f527 (diff) | |
Bug rattrapage erreur locate_reference
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5122 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6c123b8209..f0efb9db81 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -538,12 +538,14 @@ let vernac_canonical locqid = let locate_reference ref = let (loc,qid) = qualid_of_reference ref in - match Nametab.extended_locate qid with + try match Nametab.extended_locate qid with | TrueGlobal ref -> ref | SyntacticDef kn -> match Syntax_def.search_syntactic_definition loc kn with | Rawterm.RRef (_,ref) -> ref - | _ -> error_global_not_found_loc loc qid + | _ -> raise Not_found + with Not_found -> + error_global_not_found_loc loc qid let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in |