Merge PR #11715: Be robust in calculating visible ids for non-registered constants.

Reviewed-by: herbelin

3 files changed, 25 insertions, 7 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index bcc8c34a4d..d2c37fb716 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -259,15 +259,17 @@ let visible_ids sigma (nenv, c) =
     let (gseen, vseen, ids) = !accu in
     let g = global_of_constr c in
     if not (GlobRef.Set_env.mem g gseen) then
-      begin
-      try
       let gseen = GlobRef.Set_env.add g gseen in
-      let short = Nametab.shortest_qualid_of_global Id.Set.empty g in
-      let dir, id = repr_qualid short in
-      let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
+      let ids = match Nametab.shortest_qualid_of_global Id.Set.empty g with
+      | short ->
+        let dir, id = repr_qualid short in
+        if DirPath.is_empty dir then Id.Set.add id ids else ids
+      | exception Not_found ->
+        (* This may happen if given pathological terms or when manipulating
+           open modules *)
+        ids
+      in
       accu := (gseen, vseen, ids)
-      with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> ()
-      end
   | Rel p ->
     let (gseen, vseen, ids) = !accu in
     if p > n && not (Int.Set.mem p vseen) then
diff --git a/test-suite/output/bug_8206.out b/test-suite/output/bug_8206.out
new file mode 100644
index 0000000000..6015fe32f9
--- /dev/null
+++ b/test-suite/output/bug_8206.out
@@ -0,0 +1,5 @@
+File "stdin", line 11, characters 0-23:
+Error: Signature components for label homework do not match: expected type
+"forall a b : nat, bug_8206.M.add a b = bug_8206.M.add b a" but found type
+"nat -> forall b : nat, bug_8206.M.add 0 b = bug_8206.M.add b 0".
+
diff --git a/test-suite/output/bug_8206.v b/test-suite/output/bug_8206.v
new file mode 100644
index 0000000000..8d4e73dfac
--- /dev/null
+++ b/test-suite/output/bug_8206.v
@@ -0,0 +1,11 @@
+Module Type Sig.
+  Parameter add: nat -> nat -> nat.
+  Axiom homework: forall (a b: nat), add a b = add b a.
+End Sig.
+
+Module Impl.
+  Definition add(a b: nat) := plus a b.
+  Axiom homework: forall (a b: nat), add 0 b = add b 0.
+End Impl.
+
+Module M : Sig := Impl.