4 files changed, 95 insertions, 8 deletions
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index 8447cf10db..8c4808a755 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -1,17 +1,16 @@
 open Names
 
-let evil t f =
+let evil name name_f =
   let open Univ in
   let open Entries in
-  let open Decl_kinds in
   let open Constr in
-  let k = IsDefinition Definition in
+  let kind = Decls.(IsDefinition Definition) in
   let u = Level.var 0 in
   let tu = mkType (Universe.make u) in
   let te = Declare.definition_entry
       ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu
   in
-  let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in
+  let tc = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry te) in
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
@@ -19,4 +18,5 @@ let evil t f =
       ~types:(Term.mkArrowR tc tu)
       (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1))
   in
-  ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k))
+  let _ : Constant.t = Declare.declare_constant ~name:name_f ~kind (Declare.DefinitionEntry fe) in
+  ()
diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out
new file mode 100644
index 0000000000..2eadd22db8
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.out
@@ -0,0 +1,73 @@
+
+Coq < 1 subgoal
+  
+  ============================
+  forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k
+
+x < 
+x < 1 focused subgoal
+(shelved: 1)
+  
+  i : nat
+  ============================
+  exists k : nat, i = ?j /\ ?j = k /\ i = k
+
+x < 1 focused subgoal
+(shelved: 2)
+  
+  i : nat
+  ============================
+  i = ?j /\ ?j = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 2)
+  
+  i : nat
+  ============================
+  i = ?j
+
+subgoal 2 is:
+ ?j = ?k /\ i = ?k
+
+x < 1 focused subgoal
+(shelved: 1)
+  
+  i : nat
+  ============================
+  i = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 1)
+  
+  i : nat
+  ============================
+  i = ?k
+
+subgoal 2 is:
+ i = ?k
+
+x < 1 subgoal
+  
+  i : nat
+  ============================
+  i = i
+
+x < goal ID 16 at state 5
+  
+  i : nat
+  ============================
+  i = ?j /\ ?j = ?k /\ i = ?k
+
+x < goal ID 16 at state 7
+  
+  i : nat
+  ============================
+  i = i /\ i = ?k /\ i = ?k
+
+x < goal ID 16 at state 9
+  
+  i : nat
+  ============================
+  i = i /\ i = i /\ i = i
+
+x < 
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v
new file mode 100644
index 0000000000..9545254770
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.v
@@ -0,0 +1,11 @@
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.
+  eexists.
+  split.
+    trivial.
+  split.
+    trivial.
+Show Goal 16 at 5.
+Show Goal 16 at 7.
+Show Goal 16 at 9.
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index 2a7ce806d7..dc793598a9 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -1,5 +1,7 @@
 File "stdin", line 10, characters 0-28:
-Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker]
+Warning:
+New coercion path [ac; cd] : A >-> D is ambiguous with existing 
+[ab; bd] : A >-> D. [ambiguous-paths,typechecker]
 [ab] : A >-> B
 [ab; bd] : A >-> D
 [ac] : A >-> C
@@ -20,8 +22,9 @@ Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker]
 [D_B] : D >-> B
 [D_C] : D >-> C
 File "stdin", line 103, characters 0-86:
-Warning: Ambiguous paths: [D_C; C_A'] : D >-> A'
-[ambiguous-paths,typechecker]
+Warning:
+New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
+[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
 [A'_A] : A' >-> A
 [B_A'] : B >-> A'
 [B_A'; A'_A] : B >-> A