diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-08 01:46:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-08 02:00:24 +0200 |
| commit | 6e8787737a0eae9ed8aa5b1696a94495e7cb6020 (patch) | |
| tree | b6f5e9f4d6ea0461ae584fa7bec0d67fc8a2a3d4 /pretyping/program.ml | |
| parent | 9bdd8aff92829aaa7c5a45b6e4e5adfa9e8789df (diff) | |
Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.
Diffstat (limited to 'pretyping/program.ml')
| -rw-r--r-- | pretyping/program.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/program.ml b/pretyping/program.ml index b4333847b..62aedcfbf 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -15,10 +15,12 @@ open Term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = - let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in + let dp = make_dir dir in + let sp = Libnames.make_path dp (Id.of_string s) in try Nametab.global_of_path sp with Not_found -> - anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp) + user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++ + str " has to be required first.") let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) |