From 6e8787737a0eae9ed8aa5b1696a94495e7cb6020 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Oct 2016 01:46:09 +0200
Subject: Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.

---
 pretyping/program.ml          | 6 ++++--
 test-suite/bugs/closed/5066.v | 7 +++++++
 2 files changed, 11 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/5066.v

diff --git a/pretyping/program.ml b/pretyping/program.ml
index b4333847b7..62aedcfbf6 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)
diff --git a/test-suite/bugs/closed/5066.v b/test-suite/bugs/closed/5066.v
new file mode 100644
index 0000000000..eed7f0f3ff
--- /dev/null
+++ b/test-suite/bugs/closed/5066.v
@@ -0,0 +1,7 @@
+Require Import Vector.
+
+Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) :=
+  match v1 with
+  | nil _          => v2
+  | cons _ e n' sv => vector_rev sv (cons A e n2 v2)
+  end.
-- 
cgit v1.2.3