17 files changed, 419 insertions, 26 deletions
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 85ad41d1c..23a58501f 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -505,8 +505,6 @@ Qed.
 Require Export Coq.Logic.FunctionalExtensionality.
 Print PLanguage.
 
-Unset Standard Proposition Elimination Names.
-
 Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
 Transformation (PLanguage l1) (PLanguage l2) :=
   mkTransformation (PLanguage l1) (PLanguage l2)
diff --git a/test-suite/bugs/closed/6313.v b/test-suite/bugs/closed/6313.v
new file mode 100644
index 000000000..4d263c5a8
--- /dev/null
+++ b/test-suite/bugs/closed/6313.v
@@ -0,0 +1,64 @@
+(* Former open goals in nested proofs were lost *)
+
+(* This used to fail with "Incorrect number of goals (expected 1 tactic)." *)
+
+Inductive foo := a | b | c.
+Goal foo -> foo.
+  intro x.
+  simple refine (match x with
+                 | a => _
+                 | b => ltac:(exact b)
+                 | c => _
+                 end); [exact a|exact c].
+Abort.
+
+(* This used to leave the goal on the shelf and fails at reflexivity *)
+
+Goal (True/\0=0 -> True) -> True.
+  intro f.
+  refine
+   (f ltac:(split; only 1:exact I)).
+  reflexivity.
+Qed.
+
+(* The "Unshelve" used to not see the explicitly "shelved" goal *)
+
+Lemma f (b:comparison) : b=b.
+refine (match b with
+   Eq => ltac:(shelve)
+ | Lt => ltac:(give_up)
+ | Gt => _
+ end).
+exact (eq_refl Gt).
+Unshelve.
+exact (eq_refl Eq).
+Fail auto. (* Check that there are no more regular subgoals *)
+Admitted.
+
+(* The "Unshelve" used to not see the explicitly "shelved" goal *)
+
+Lemma f2 (b:comparison) : b=b.
+refine (match b with
+   Eq => ltac:(shelve)
+ | Lt => ltac:(give_up)
+ | Gt => _
+ end).
+Unshelve. (* Note: Unshelve puts goals at the end *)
+exact (eq_refl Gt).
+exact (eq_refl Eq).
+Fail auto. (* Check that there are no more regular subgoals *)
+Admitted.
+
+(* The "unshelve" used to not see the explicitly "shelved" goal *)
+
+Lemma f3 (b:comparison) : b=b.
+unshelve refine (match b with
+   Eq => ltac:(shelve)
+ | Lt => ltac:(give_up)
+ | Gt => _
+ end).
+(* Note: unshelve puts goals at the beginning *)
+exact (eq_refl Eq).
+exact (eq_refl Gt).
+Fail auto. (* Check that there are no more regular subgoals *)
+Admitted.
diff --git a/test-suite/bugs/closed/6634.v b/test-suite/bugs/closed/6634.v
new file mode 100644
index 000000000..7f33afcc2
--- /dev/null
+++ b/test-suite/bugs/closed/6634.v
@@ -0,0 +1,6 @@
+From Coq Require Import ssreflect.
+
+Lemma normalizeP (p : tt = tt) : p = p.
+Proof.
+Fail move: {2} tt p.
+Abort.
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v
index 0b576db6b..820022d99 100644
--- a/test-suite/bugs/opened/1596.v
+++ b/test-suite/bugs/opened/1596.v
@@ -2,7 +2,6 @@ Require Import Relations.
 Require Import FSets.
 Require Import Arith.
 Require Import Omega.
-Unset Standard Proposition Elimination Names.
 
 Set Keyed Unification.
 
diff --git a/test-suite/failure/fixpointeta.v b/test-suite/failure/fixpointeta.v
new file mode 100644
index 000000000..9af719322
--- /dev/null
+++ b/test-suite/failure/fixpointeta.v
@@ -0,0 +1,70 @@
+
+Set Primitive Projections.
+
+Record R := C { p : nat }.
+(* R is defined
+p is defined *)
+
+Unset Primitive Projections.
+Record R' := C' { p' : nat }.
+
+
+
+Fail Definition f := fix f (x : R) : nat := p x.
+(** Not allowed to make fixpoint defs on (non-recursive) records
+  having eta *)
+
+Fail Definition f := fix f (x : R') : nat := p' x.
+(** Even without eta (R' is not primitive here), as long as they're
+  found to be BiFinite (non-recursive), we disallow it *)
+
+(*
+
+(* Subject reduction failure example, if we allowed fixpoints *)
+
+Set Primitive Projections.
+
+Record R := C { p : nat }.
+
+Definition f := fix f (x : R) : nat := p x.
+
+(* eta rule for R *)
+Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x
+ := v.
+
+Definition goal := forall x, f x = p x.
+
+(* when we compute the Rtr away typechecking will fail *)
+Definition thing : goal := fun x =>
+(Rtr (fun x => f x = p x) x (eq_refl _)).
+
+Definition thing' := Eval compute in thing.
+
+Fail Check (thing = thing').
+(*
+The command has indeed failed with message:
+The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
+while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)"
+and "f x = p x").
+*)
+
+Definition thing_refl := eq_refl thing.
+
+Fail Definition thing_refl' := Eval compute in thing_refl.
+(*
+The command has indeed failed with message:
+Illegal application:
+The term "@eq_refl" of type "forall (A : Type) (x : A), x = x"
+cannot be applied to the terms
+ "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop"
+ "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
+The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
+which should be coercible to
+ "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)".
+ *)
+
+Definition more_refls : thing_refl = thing_refl.
+Proof.
+  compute. reflexivity.
+Fail Defined. Abort.
+ *)
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index abf8be72e..d163dfbcd 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -40,7 +40,7 @@ Proof.
 Qed.
 
 
-Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z.
+Lemma QdenZpower : forall x : Q, Zpos (Qden (x ^ 2)%Q) = (Zpos (Qden x) ^ 2) %Z.
 Proof.
   intros.
   destruct x.
@@ -54,9 +54,9 @@ Qed.
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
  unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq.
- assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
+ assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
  assert (Hnx : (Qnum x <> 0)%Z)
  by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
- apply integer_statement; exists (Qnum x); exists (' Qden x); auto.
+ apply integer_statement; exists (Qnum x); exists (Zpos (Qden x)); auto.
 Qed.
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/UnivBinders.out b/test-suite/output/UnivBinders.out
index 668b4e578..6f41b2fcf 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -149,24 +149,24 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
-(* i Top.41 Top.42 |=  *)
+axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i}
+(* i Top.44 Top.45 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
-(* i Top.41 Top.42 |=  *)
+axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i}
+(* i Top.44 Top.45 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.44} -> Type@{axbar'.i}
+axfoo' : Type@{Top.47} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.44} -> Type@{axbar'.i}
+axbar' : Type@{Top.47} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 266d94ad9..c6efc240a 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -44,6 +44,9 @@ Module mono.
 
   Monomorphic Definition monomono := Type@{MONOU}.
   Check monomono.
+
+  Monomorphic Inductive monoind@{i} : Type@{i} := .
+  Monomorphic Record monorecord@{i} : Type@{i} := mkmonorecord {}.
 End mono.
 Check mono.monomono. (* qualified MONOU *)
 Import mono.
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]
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 6962e43e7..8d08f5975 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 000000000..e34c240c5
--- /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.
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index e05762477..4dda36042 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -134,3 +134,24 @@ Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparam
 
 Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j}
   := fun x => x.
+
+(** Cumulative constructors *)
+
+
+Record twotys@{u v w} : Type@{w} :=
+  twoconstr { fstty : Type@{u}; sndty : Type@{v} }.
+
+Monomorphic Universes i j k l.
+
+Monomorphic Constraint i < j.
+Monomorphic Constraint j < k.
+Monomorphic Constraint k < l.
+
+Parameter Tyi : Type@{i}.
+
+Definition checkcumul :=
+  eq_refl _ : @eq twotys@{k k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi).
+
+(* They can only be compared at the highest type *)
+Fail Definition checkcumul' :=
+  eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi).
diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v
new file mode 100644
index 000000000..571dde880
--- /dev/null
+++ b/test-suite/success/name_mangling.v
@@ -0,0 +1,192 @@
+(* -*- coq-prog-args: ("-mangle-names" "_") -*- *)
+
+(* Check that refine policy of redefining previous names make these names private *)
+(* abstract can change names in the environment! See bug #3146 *)
+
+Goal True -> True.
+intro.
+Fail exact H.
+exact _0.
+Abort.
+
+Unset Mangle Names.
+Goal True -> True.
+intro; exact H.
+Abort.
+
+Set Mangle Names.
+Set Mangle Names Prefix "baz".
+Goal True -> True.
+intro.
+Fail exact H.
+Fail exact _0.
+exact baz0.
+Abort.
+
+Goal True -> True.
+intro; assumption.
+Abort.
+
+Goal True -> True.
+intro x; exact x.
+Abort.
+
+Goal forall x y, x+y=0.
+intro x.
+refine (fun x => _).
+Fail Check x0.
+Check x.
+Abort.
+
+(* Example from Emilio *)
+
+Goal forall b : False, b = b.
+intro b.
+refine (let b := I in _).
+Fail destruct b0.
+Abort.
+
+(* Example from Cyprien *)
+
+Goal True -> True.
+Proof.
+  refine (fun _ => _).
+  Fail exact t.
+Abort.
+
+(* Example from Jason *)
+
+Goal False -> False.
+intro H.
+Fail abstract exact H.
+Abort.
+
+(* Variant *)
+
+Goal False -> False.
+intro.
+Fail abstract exact H.
+Abort.
+
+(* Example from Jason *)
+
+Goal False -> False.
+intro H.
+(* Name H' is from Ltac here, so it preserves the privacy *)
+(* But abstract messes everything up *)
+Fail let H' := H in abstract exact H'.
+let H' := H in exact H'.
+Qed.
+
+(* Variant *)
+
+Goal False -> False.
+intro.
+Fail let H' := H in abstract exact H'.
+Abort.
+
+(* Indirectly testing preservation of names by move (derived from Jason) *)
+
+Inductive nat2 := S2 (_ _ : nat2).
+Goal forall t : nat2, True.
+  intro t.
+  let IHt1 := fresh "IHt1" in
+  let IHt2 := fresh "IHt2" in
+  induction t as [? IHt1 ? IHt2].
+  Fail exact IHt1.
+Abort.
+
+(* Example on "pose proof" (from Jason) *)
+
+Goal False -> False.
+intro; pose proof I as H0.
+Fail exact H.
+Abort.
+
+(* Testing the approach for which non alpha-renamed quantified names are user-generated *)
+
+Section foo.
+Context (b : True).
+Goal forall b : False, b = b.
+Fail destruct b0.
+Abort.
+
+Goal forall b : False, b = b.
+now destruct b.
+Qed.
+End foo.
+
+(* Test stability of "fix" *)
+
+Lemma a : forall n, n = 0.
+Proof.
+fix a 1.
+Check a.
+fix 1.
+Fail Check a0.
+Abort.
+
+(* Test stability of "induction" *)
+
+Lemma a : forall n : nat, n = n.
+Proof.
+intro n; induction n as [ | n IHn ].
+- auto.
+- Check n.
+  Check IHn.
+Abort.
+
+Inductive I := C : I -> I -> I.
+
+Lemma a : forall n : I, n = n.
+Proof.
+intro n; induction n as [ n1 IHn1 n2 IHn2 ].
+Check n1.
+Check n2.
+apply f_equal2.
++ apply IHn1.
++ apply IHn2.
+Qed.
+
+(* Testing remember *)
+
+Lemma c : 0 = 0.
+Proof.
+remember 0 as x eqn:Heqx.
+Check Heqx.
+Abort.
+
+Lemma c : forall Heqx, Heqx -> 0 = 0.
+Proof.
+intros Heqx X.
+remember 0 as x.
+Fail Check Heqx0. (* Heqx0 is not canonical *)
+Abort.
+
+(* An example by Jason from the discussion for PR #268 *)
+
+Goal nat -> Set -> True.
+  intros x y.
+  match goal with
+  | [ x : _, y : _ |- _ ]
+    => let z := fresh "z" in
+      rename y into z, x into y;
+        let x' := fresh "x" in
+        rename z into x'
+  end.
+  revert y. (* x has been explicitly moved to y *)
+  Fail revert x. (* x comes from "fresh" *)
+Abort.
+
+Goal nat -> Set -> True.
+  intros.
+  match goal with
+  | [ x : _, y : _ |- _ ]
+    => let z := fresh "z" in
+      rename y into z, x into y;
+        let x' := fresh "x" in
+        rename z into x'
+  end.
+  Fail revert y. (* generated by intros *)
+  Fail revert x. (* generated by intros *)
+Abort.
diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v
index 3f6b9cb39..916bb846a 100644
--- a/test-suite/success/shrink_abstract.v
+++ b/test-suite/success/shrink_abstract.v
@@ -1,5 +1,3 @@
-Set Shrink Abstract.
-
 Definition foo : forall (n m : nat), bool.
 Proof.
 pose (p := 0).