3 files changed, 23 insertions, 10 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index afc1c4caf..dd8a48b85 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -149,17 +149,8 @@ let extern_evar loc n l = CEvar (loc,n,l)
     For instance, in the debugger the tables of global references
     may be inaccurate *)
 
-let safe_shortest_qualid_of_global vars r =
-  try shortest_qualid_of_global vars r
-  with Not_found ->
-    match r with
-    | VarRef v -> make_qualid DirPath.empty v
-    | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c))
-    | IndRef (i,_) | ConstructRef ((i,_),_) ->
-        make_qualid DirPath.empty Names.(Label.to_id (mind_label i))
-
 let default_extern_reference loc vars r =
-  Qualid (loc,safe_shortest_qualid_of_global vars r)
+  Qualid (loc,shortest_qualid_of_global vars r)
 
 let my_extern_reference = ref default_extern_reference
 
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 000000000..3cf3c2d8f
--- /dev/null
+++ b/test-suite/output/qualification.out
@@ -0,0 +1,3 @@
+File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7:
+Error: Signature components for label test do not match: expected type
+"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v
new file mode 100644
index 000000000..d39097e2d
--- /dev/null
+++ b/test-suite/output/qualification.v
@@ -0,0 +1,19 @@
+Module Type T1.
+  Parameter t : Type.
+End T1.
+
+Module Type T2.
+  Declare Module M : T1.
+  Parameter t : Type.
+  Parameter test : t = M.t.
+End T2.
+
+Module M1 <: T1.
+  Definition t : Type := bool.
+End M1.
+
+Module M2 <: T2.
+  Module M := M1.
+  Definition t : Type := nat.
+  Lemma test : t = t. Proof. reflexivity. Qed.
+End M2.