6 files changed, 54 insertions, 12 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 4df21ae353..e73312c679 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 9680d2bbff..18f5d89f66 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 e6a6e0288a..864b6151a1 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 d28ee42761..5e9eff0481 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]
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 6962e43e7e..8d08f5975e 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -172,3 +172,14 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
   Timeout 1 Fail apply _. (* 0.06s *)
 Abort.
 End HintCut.
+
+
+(* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *)
+(* e.g. those tactics when considering a goal with existential varibles *)
+(* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *)
+(* See this Coq club post for more detail: *)
+(* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *)
+
+Goal forall (m : nat), exists n, m = n /\ m = n.
+  intros m; eexists; split; [trivial | reflexivity].
+Qed.
diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v
new file mode 100644
index 0000000000..e34c240c5d
--- /dev/null
+++ b/test-suite/success/ShowExtraction.v
@@ -0,0 +1,31 @@
+
+Require Extraction.
+Require Import List.
+
+Section Test.
+Variable A : Type.
+Variable decA : forall (x y:A), {x=y}+{x<>y}.
+
+(** Should fail when no proofs are started *)
+Fail Show Extraction.
+
+Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}.
+Proof.
+Show Extraction.
+fix 1.
+destruct xs as [|x xs], ys as [|y ys].
+Show Extraction.
+- now left.
+- now right.
+- now right.
+- Show Extraction.
+  destruct (decA x y).
+  + destruct (decListA xs ys).
+    * left; now f_equal.
+    * Show Extraction.
+      right. congruence.
+  + right. congruence.
+Show Extraction.
+Defined.
+
+End Test.