diff options
| author | herbelin | 2001-09-07 13:07:17 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-07 13:07:17 +0000 |
| commit | 47d1e4d9d09dee1fccce3e2d7b1c7330440bd318 (patch) | |
| tree | 05b1a2c365530a8b517f1ac8a678900b9e3066b3 /toplevel | |
| parent | 18e28049e62ce80a45c8f7bd6f496b502caa8ad1 (diff) | |
Suppression des library roots, on teste si un nom est absolu autrement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1927 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/errors.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernacinterp.ml | 2 |
3 files changed, 10 insertions, 4 deletions
diff --git a/toplevel/errors.ml b/toplevel/errors.ml index 11e7c38ccd..cf48f0764c 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -81,6 +81,9 @@ let rec explain_exn_default = function 'sTR "The reference"; 'sPC; Nametab.pr_qualid q; 'sPC ; 'sTR "was not found"; 'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >] + | Nametab.GlobalizationConstantError q -> + hOV 0 [< 'sTR "Error:"; 'sPC; + 'sTR "No constant of this name:"; 'sPC; Nametab.pr_qualid q >] | Tacmach.FailError i -> hOV 0 [< 'sTR "Error: Fail tactic always fails (level "; 'iNT i; 'sTR")." >] diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 82d31cf641..7618aadd71 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -179,11 +179,14 @@ let msg_found_library = function let msg_notfound_library qid = function | Library.LibUnmappedDir -> let dir = fst (Nametab.repr_qualid qid) in - mSG [< 'sTR "No physical path is bound to "; pr_dirpath dir; 'fNL >] + errorlabstrm "locate_library" + [< 'sTR "Cannot find a physical path bound to logical path "; + pr_dirpath dir; 'fNL >] | Library.LibNotFound -> mSG (hOV 0 - [< 'sTR"Unable to locate library"; 'sPC; Nametab.pr_qualid qid; 'fNL >]) - | _ -> assert false + [< 'sTR"Unable to locate library"; + 'sPC; Nametab.pr_qualid qid; 'fNL >]) + | e -> assert false let _ = add "LocateLibrary" diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index f1d38494f4..3d170e6bed 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -89,7 +89,7 @@ let rec cvt_varg ast = let q = Astterm.interp_qualid p in let sp = try Nametab.locate_constant q - with Not_found -> Nametab.error_global_not_found_loc loc q + with Not_found -> Nametab.error_global_constant_not_found_loc loc q in VARG_CONSTANT sp | Str(_,s) -> VARG_STRING s | Id(_,s) -> VARG_STRING s |