From fd39a2e844f93b314c2f0b78510f0573cfa1bef3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 6 Oct 2016 19:34:28 +0200
Subject: Revert "Make the pretty printer resilient to incomplete nametab
 (progress on #4363)."

This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402.

This fixes bug #4874. We fallback to the original error message of v8.4.
The fallback printer introduced in this commit only gave unqualified names,
which is what this bug reports.
---
 interp/constrextern.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 68a3cf0f4a..ae9b5bace2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -147,17 +147,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
 
-- 
cgit v1.2.3


From 159b10655172b6f0888f9622be3620c3c33d35b1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Oct 2016 12:17:01 +0200
Subject: Test for bug #4874.

---
 test-suite/output/qualification.out |  3 +++
 test-suite/output/qualification.v   | 19 +++++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 test-suite/output/qualification.out
 create mode 100644 test-suite/output/qualification.v

diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 0000000000..3cf3c2d8fb
--- /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 0000000000..d39097e2dd
--- /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.
-- 
cgit v1.2.3