Adding mention of shelved/given-up status in "Show Existentials".

Also changed the API of pr_subgoals now using labels.

Also removed a trailing space in printing existentials.

4 files changed, 12 insertions, 12 deletions

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 4df21ae35..e73312c67 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -11,7 +11,7 @@ notation scopes add ': clear scopes' [arguments-assert,vernacular]
 eq_refl
      : ?y = ?y
 where
-?y : [ |- nat] 
+?y : [ |- nat]
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq_refl: Arguments are renamed to B, y
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 9680d2bbf..18f5d89f6 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,4 +1,4 @@
-Existential 1 = ?Goal : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
+Existential 1 = ?Goal : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m]
 Existential 2 =
-?y : [p : nat  q := S p : nat  n : nat  m : nat |- nat] (p, q cannot be used)
-Existential 3 = ?Goal0 : [q : nat  n : nat  m : nat |- n = ?y] 
+?y : [p : nat  q := S p : nat  n : nat  m : nat |- nat] (p, q cannot be used) (shelved)
+Existential 3 = ?Goal0 : [q : nat  n : nat  m : nat |- n = ?y]
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e6a6e0288..864b6151a 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -33,24 +33,24 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
      : (forall x : nat * (bool * unit), ?T) ->
        forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
 where
-?T : [x : nat * (bool * unit) |- Type] 
+?T : [x : nat * (bool * unit) |- Type]
 fun f : forall x : bool * (nat * unit), ?T =>
 CURRYINV (x : nat) (y : bool), f
      : (forall x : bool * (nat * unit), ?T) ->
        forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))}
 where
-?T : [x : bool * (nat * unit) |- Type] 
+?T : [x : bool * (nat * unit) |- Type]
 fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f
      : (forall x : unit * nat * bool, ?T) ->
        forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)}
 where
-?T : [x : unit * nat * bool |- Type] 
+?T : [x : unit * nat * bool |- Type]
 fun f : forall x : unit * bool * nat, ?T =>
 CURRYINVLEFT (x : nat) (y : bool), f
      : (forall x : unit * bool * nat, ?T) ->
        forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)}
 where
-?T : [x : unit * bool * nat |- Type] 
+?T : [x : unit * bool * nat |- Type]
 forall n : nat, {#n | 1 > n}
      : Prop
 forall x : nat, {|x | x > 0|}
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index d28ee4276..5e9eff048 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
 fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where
-?t : [n : nat  y := A n : T n |- ?T -> T n] 
-?x : [n : nat  y := A n : T n |- ?T] 
+?t : [n : nat  y := A n : T n |- ?T -> T n]
+?x : [n : nat  y := A n : T n |- ?T]
 fun n : nat => ?t ?x : T n
      : forall n : nat, T n
 where
-?t : [n : nat |- ?T -> T n] 
-?x : [n : nat |- ?T] 
+?t : [n : nat |- ?T -> T n]
+?x : [n : nat |- ?T]