[ssr] import ssreflect test suite from math-comp

43 files changed, 2122 insertions, 0 deletions

diff --git a/test-suite/ssr/absevarprop.v b/test-suite/ssr/absevarprop.v
new file mode 100644
index 000000000..fa1de0095
--- /dev/null
+++ b/test-suite/ssr/absevarprop.v
@@ -0,0 +1,96 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect ssrbool ssrfun.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Lemma test15: forall (y : nat) (x : 'I_2), y < 1 -> val x = y -> Some x = insub y.
+move=> y x le_1 defx; rewrite insubT ?(leq_trans le_1) // => ?.
+by congr (Some _); apply: val_inj=> /=; exact: defx.
+Qed.
+
+Axiom P : nat -> Prop.
+Axiom Q : forall n, P n -> Prop.
+Definition R := fun (x : nat) (p : P x) m (q : P (x+1)) => m > 0.
+
+Inductive myEx : Type := ExI : forall n (pn : P n) pn', Q n pn -> R n pn n pn' -> myEx.
+
+Variable P1 : P 1.
+Variable P11 : P (1 + 1).
+Variable Q1 : forall P1, Q 1 P1.
+
+Lemma testmE1 : myEx.
+Proof.
+apply: ExI 1 _ _ _ _.
+  match goal with |- P 1 => exact: P1 | _ => fail end.
+  match goal with |- P (1+1) => exact: P11 | _ => fail end.
+  match goal with |- forall p : P 1, Q 1 p => move=> *; exact: Q1 | _ => fail end.
+match goal with |- forall (p : P 1) (q : P (1+1)), is_true (R 1 p 1 q) => done | _ => fail end.
+Qed.
+
+Lemma testE2 : exists y : { x | P x }, sval y = 1.
+Proof.
+apply: ex_intro (exist _ 1 _) _.
+  match goal with |- P 1 => exact: P1 | _ => fail end.
+match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end.
+Qed.
+
+Lemma testE3 : exists y : { x | P x }, sval y = 1.
+Proof.
+have := (ex_intro _ (exist _ 1 _) _); apply.
+  match goal with |- P 1 => exact: P1 | _ => fail end.
+match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end.
+Qed.
+
+Lemma testE4 : P 2 -> exists y : { x | P x }, sval y = 2.
+Proof.
+move=> P2; apply: ex_intro (exist _ 2 _) _.
+match goal with |- @sval _ _ (@exist _ _ 2 P2) = 2 => done | _ => fail end.
+Qed.
+
+Hint Resolve P1.
+
+Lemma testmE12 : myEx.
+Proof.
+apply: ExI 1 _ _ _ _.
+  match goal with |- P (1+1) => exact: P11 | _ => fail end.
+  match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
+match goal with |- forall (q : P (1+1)), is_true (R 1 P1 1 q) => done | _ => fail end.
+Qed.
+
+Create HintDb SSR.
+
+Hint Resolve P11 : SSR.
+
+Ltac ssrautoprop := trivial with SSR.
+
+Lemma testmE13 : myEx.
+Proof.
+apply: ExI 1 _ _ _ _.
+  match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
+match goal with |- is_true (R 1 P1 1 P11) => done | _ => fail end.
+Qed.
+
+Definition R1 := fun (x : nat) (p : P x) m (q : P (x+1)) (r : Q x p) => m > 0.
+
+Inductive myEx1 : Type :=
+  ExI1 : forall n (pn : P n) pn' (q : Q n pn), R1 n pn n pn' q -> myEx1.
+
+Hint Resolve (Q1 P1) : SSR.
+
+(* tests that goals in prop are solved in the right order, propagating instantiations,
+   thus the goal Q 1 ?p1 is faced by trivial after ?p1, and is thus evar free *)
+Lemma testmE14 : myEx1.
+Proof.
+apply: ExI1 1 _ _ _ _.
+match goal with |- is_true (R1 1 P1 1 P11 (Q1 P1)) => done | _ => fail end.
+Qed.
diff --git a/test-suite/ssr/abstract_var2.v b/test-suite/ssr/abstract_var2.v
new file mode 100644
index 000000000..7c57d2024
--- /dev/null
+++ b/test-suite/ssr/abstract_var2.v
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import ssreflect.
+
+Set Implicit Arguments.
+
+Axiom P : nat -> nat -> Prop.
+
+Axiom tr :
+  forall x y z, P x y -> P y z -> P x z.
+
+Lemma test a b c : P a c -> P a b.
+Proof.
+intro H.
+Fail have [: s1 s2] H1 : P a b := @tr _ _ _ s1 s2.
+have [: w s1 s2] H1 : P a b := @tr _ w _ s1 s2.
+Abort.
diff --git a/test-suite/ssr/binders.v b/test-suite/ssr/binders.v
new file mode 100644
index 000000000..97b7d830f
--- /dev/null
+++ b/test-suite/ssr/binders.v
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Lemma test (x : bool) : True.
+have H1 x := x.
+have (x) := x => H2.
+have H3 T (x : T) := x.
+have ? : bool := H1 _ x.
+have ? : bool := H2 _ x.
+have ? : bool := H3 _ x.
+have ? (z : bool) : forall y : bool, z = z := fun y => refl_equal _.
+have ? w : w = w := @refl_equal nat w.
+have ? y : true by [].
+have ? (z : bool) : z = z.
+  exact: (@refl_equal _ z).
+have ? (z w : bool) : z = z by exact: (@refl_equal _ z).
+have H w (a := 3) (_ := 4) : w && true = w.
+  by rewrite andbT.
+exact I.
+Qed.
+
+Lemma test1 : True.
+suff (x : bool): x = x /\ True.
+  by move/(_ true); case=> _.
+split; first by exact: (@refl_equal _ x).
+suff H y : y && true = y /\ True.
+  by case: (H true).
+suff H1 /= : true && true /\ True.
+  by rewrite andbT; split; [exact: (@refl_equal _ y) | exact: I].
+match goal with |- is_true true /\ True => idtac end.
+by split.
+Qed.
+
+Lemma foo n : n >= 0.
+have f i (j := i + n) : j < n.
+  match goal with j := i + n |- _ => idtac end.
+Undo 2.
+suff f i (j := i + n) : j < n.
+  done.
+match goal with j := i + n |- _ => idtac end.
+Undo 3.
+done.
+Qed.
diff --git a/test-suite/ssr/binders_of.v b/test-suite/ssr/binders_of.v
new file mode 100644
index 000000000..69b52eace
--- /dev/null
+++ b/test-suite/ssr/binders_of.v
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+
+Require Import ssreflect.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : True.
+have f of seq nat & nat : nat.
+  exact 3.
+have g of nat := 3.
+have h of nat : nat := 3.
+have _ : f [::] 3 = g 3 + h 4.
+Admitted.
diff --git a/test-suite/ssr/caseview.v b/test-suite/ssr/caseview.v
new file mode 100644
index 000000000..94b064b02
--- /dev/null
+++ b/test-suite/ssr/caseview.v
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+
+Lemma test (A B : Prop) : A /\ B -> True.
+Proof. by case=> _ /id _. Qed.
diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v
new file mode 100644
index 000000000..7e60b04a6
--- /dev/null
+++ b/test-suite/ssr/congr.v
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : forall a b : nat, a == b -> a == 0 -> b == 0.
+Proof. move=> a b Eab Eac; congr (_ == 0) : Eac; exact: eqP Eab. Qed.
+
+Definition arrow A B := A -> B.
+
+Lemma test2 : forall a b : nat, a == b -> arrow (a == 0) (b == 0).
+Proof. move=> a b Eab; congr (_ == 0); exact: eqP Eab. Qed.
+
+Definition equals T (A B : T) := A = B.
+
+Lemma test3 : forall a b : nat, a = b -> equals nat (a + b) (b + b).
+Proof. move=> a b E; congr (_ + _); exact E. Qed.
+
+Variable S : eqType.
+Variable f : nat -> S.
+Coercion f : nat >-> Equality.sort.
+
+Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a).
+Proof. move=> a b Eba; congr (_ + _); exact:  Eba. Qed.
diff --git a/test-suite/ssr/deferclear.v b/test-suite/ssr/deferclear.v
new file mode 100644
index 000000000..85353dadf
--- /dev/null
+++ b/test-suite/ssr/deferclear.v
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Variable T : Type.
+
+Lemma test0 : forall a b c d : T, True.
+Proof. by move=> a b {a} a c; exact I. Qed.
+
+Variable P : T -> Prop.
+
+Lemma test1 : forall a b c : T, P a -> forall d : T, True.
+Proof. move=> a b {a} a _ d; exact I. Qed.
+
+Definition Q := forall x y : nat, x = y.
+Axiom L : 0 = 0 -> Q.
+Axiom L' : 0 = 0 -> forall x y : nat, x = y.
+Lemma test3 : Q.
+by apply/L.
+Undo.
+rewrite /Q.
+by apply/L.
+Undo 2.
+by apply/L'.
+Qed.
diff --git a/test-suite/ssr/dependent_type_err.v b/test-suite/ssr/dependent_type_err.v
new file mode 100644
index 000000000..a5789d8dd
--- /dev/null
+++ b/test-suite/ssr/dependent_type_err.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+
+Lemma ltn_leq_trans : forall n m p : nat, m < n -> n <= p -> m < p.
+move=> n m p Hmn Hnp; rewrite -ltnS.
+Fail rewrite (_ : forall n0 m0 p0 : nat, m0 <= n0 -> n0 < p0 -> m0 < p0).
+Fail rewrite leq_ltn_trans.
+Admitted.
diff --git a/test-suite/ssr/derive_inversion.v b/test-suite/ssr/derive_inversion.v
new file mode 100644
index 000000000..abf63a20c
--- /dev/null
+++ b/test-suite/ssr/derive_inversion.v
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import ssreflect ssrbool.
+
+Set Implicit Arguments.
+
+  Inductive wf T : bool -> option T -> Type :=
+  | wf_f : wf false None
+  | wf_t : forall x, wf true (Some x).
+
+  Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop.
+
+  Lemma Problem T b (o : option T) :
+    wf b o ->
+    match b with
+    | true  => exists x, o = Some x
+    | false => o = None
+    end.
+  Proof.
+  by case: b; elim/wf_inv=> //; case: o=> // a *; exists a.
+  Qed.
diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v
new file mode 100644
index 000000000..908249a36
--- /dev/null
+++ b/test-suite/ssr/elim.v
@@ -0,0 +1,279 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool ssrfun TestSuite.ssr_mini_mathcomp.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+(* Ltac debugging feature: recursive elim + eq generation *)
+Lemma testL1 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; elim branch: s => [|x xs _].
+match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
+match goal with _ : _ =  _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
+Qed.
+
+(* The same but with explicit eliminator and a conflict in the intro pattern *)
+Lemma testL2 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; elim/last_ind branch: s => [|x s _].
+match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
+match goal with _ : _ =  rcons _ _ |- rcons _ _ = rcons _ _ => move: branch => // | _ => fail end.
+Qed.
+
+(* The same but without names for variables involved in the generated eq *)
+Lemma testL3 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; elim branch: s; move: (s) => _.
+match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
+move=> _; match goal with _ : _ =  _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
+Qed.
+
+Inductive foo : Type := K1 : foo | K2 : foo -> foo -> foo | K3 : (nat -> foo) -> foo.
+
+(* The same but with more intros to be done *)
+Lemma testL4 : forall (o : foo), o = o.
+Proof.
+move=> o; elim branch: o.
+match goal with _ : _ = K1 |- K1 = K1 => move: branch => // | _ => fail end.
+move=> _; match goal with _ : _ = K2 _ _ |- K2 _ _ = K2 _ _ => move: branch => // | _ => fail end.
+move=> _; match goal with _ : _ =  K3 _ |- K3 _ = K3 _ => move: branch => // | _ => fail end.
+Qed.
+
+(* Occurrence counting *)
+Lemma testO1: forall (b : bool), b = b.
+Proof.
+move=> b; case: (b) / idP.
+match goal with |- is_true b -> true = true => done | _ => fail end.
+match goal with |- ~ is_true b -> false = false => done | _ => fail end.
+Qed.
+
+(* The same but only the second occ *)
+Lemma testO2: forall (b : bool), b = b.
+Proof.
+move=> b; case: {2}(b) / idP.
+match goal with |- is_true b -> b = true => done | _ => fail end.
+match goal with |- ~ is_true b -> b = false => move/(introF idP) => // | _ => fail end.
+Qed.
+
+(* The same but with eq generation *)
+Lemma testO3: forall (b : bool), b = b.
+Proof.
+move=> b; case E: {2}(b) / idP.
+match goal with _ : is_true b, _ : b = true |- b = true => move: E => _; done | _ => fail end.
+match goal with H : ~ is_true b, _ : b = false |- b = false => move: E => _; move/(introF idP): H => // | _ => fail end.
+Qed.
+
+(* Views *)
+Lemma testV1 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; case/lastP E: {1}s => [| x xs].
+match goal with _ : s = [::] |- [::] = s => symmetry; exact E | _ => fail end.
+match goal with _ : s = rcons x xs |- rcons _ _ = s => symmetry; exact E | _ => fail end.
+Qed.
+
+Lemma testV2 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; case/lastP E: s => [| x xs].
+match goal with _ : s = [::] |- [::] = [::] => done | _ => fail end.
+match goal with _ : s = rcons x xs |- rcons _ _ = rcons _ _ => done | _ => fail end.
+Qed.
+
+Lemma testV3 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; case/lastP: s => [| x xs].
+match goal with |- [::] = [::] => done | _ => fail end.
+match goal with |- rcons _ _ = rcons _ _ => done | _ => fail end.
+Qed.
+
+(* Patterns *)
+Lemma testP1: forall (x y : nat), (y == x) && (y == x) -> y == x.
+move=> x y; elim: {2}(_ == _) / eqP.
+match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end.
+match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end.
+Qed.
+
+(* The same but with an implicit pattern *)
+Lemma testP2 : forall (x y : nat), (y == x) && (y == x) -> y == x.
+move=> x y; elim: {2}_ / eqP.
+match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end.
+match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end.
+Qed.
+
+(* The same but with an eq generation switch *)
+Lemma testP3 : forall (x y : nat), (y == x) && (y == x) -> y == x.
+move=> x y; elim E: {2}_ / eqP.
+match goal with _ : y = x |- (is_true ((y == x) && true) -> is_true (y == x)) => rewrite E; reflexivity | _ => fail end.
+match goal with _ : y <> x |- (is_true ((y == x) && false) -> is_true (y == x)) => rewrite E => /= H; exact H  | _ => fail end.
+Qed.
+
+Inductive spec : nat -> nat -> nat -> Prop :=
+| specK : forall a b c, a = 0 -> b = 2 -> c = 4 -> spec a b c.
+Lemma specP : spec 0 2 4. Proof. by constructor. Qed.
+
+Lemma testP4 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: specP => a b c defa defb defc.
+match goal with |- (a.+1 + a.+1) * c = b + (a.+1 + a.+1) + (b + b) => subst; done | _ => fail end.
+Qed.
+
+Lemma testP5 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: (1 + 1) _ / specP => a b c defa defb defc.
+match goal with |- b * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end.
+Qed.
+
+Lemma testP6 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: {2}(1 + 1) _ / specP => a b c defa defb defc.
+match goal with |- (a.+1 + a.+1) * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end.
+Qed.
+
+Lemma testP7 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: _ (1 + 1) (2 + _) / specP => a b c defa defb defc.
+match goal with |- b * a.+4 = c + c => subst; done | _ => fail end.
+Qed.
+
+Lemma testP8 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case E: (1 + 1) (2 + _) / specP=> [a b c defa defb defc].
+match goal with |- b * a.+4 = c + c => subst; done | _ => fail end.
+Qed.
+
+Variables (T : Type) (tr : T -> T).
+
+Inductive exec (cf0 cf1 : T) : seq T -> Prop :=
+| exec_step : tr cf0 = cf1 -> exec cf0 cf1 [::]
+| exec_star : forall cf2 t, tr cf0 = cf2 ->
+  exec cf2 cf1 t -> exec cf0 cf1 (cf2 :: t).
+
+Inductive execr (cf0 cf1 : T) : seq T -> Prop :=
+| execr_step : tr cf0 = cf1 -> execr cf0 cf1 [::]
+| execr_star : forall cf2 t, execr cf0 cf2 t ->
+  tr cf2 = cf1 -> execr cf0 cf1 (t ++ [:: cf2]).
+
+Lemma execP : forall cf0 cf1 t, exec cf0 cf1 t <-> execr cf0 cf1 t.
+Proof.
+move=> cf0 cf1 t; split => [] Ecf.
+  elim: Ecf.
+    match goal with |- forall cf2 cf3 : T, tr cf2 = cf3 ->
+      execr cf2 cf3 [::] => myadmit | _ => fail end.
+  match goal with |- forall (cf2 cf3 cf4 : T) (t0 : seq T),
+   tr cf2 = cf4 -> exec cf4 cf3 t0 -> execr cf4 cf3 t0 ->
+   execr cf2 cf3 (cf4 :: t0) => myadmit | _ => fail end.
+elim: Ecf.
+  match goal with |- forall cf2 : T,
+    tr cf0 = cf2 -> exec cf0 cf2 [::] => myadmit | _ => fail end.
+match goal with |- forall (cf2 cf3 : T) (t0 : seq T),
+ execr cf0 cf3 t0 -> exec cf0 cf3 t0 -> tr cf3 = cf2 ->
+ exec cf0 cf2 (t0 ++ [:: cf3]) => myadmit | _ => fail end.
+Qed.
+
+Fixpoint plus (m n : nat) {struct n} : nat :=
+   match n with
+   | 0 => m
+   | S p => S (plus m p)
+   end.
+
+Definition plus_equation :
+forall m n : nat,
+       plus m n =
+       match n with
+       | 0 => m
+       | p.+1 => (plus m p).+1
+       end
+:=
+fun m n : nat =>
+match
+  n as n0
+  return
+    (forall m0 : nat,
+     plus m0 n0 =
+     match n0 with
+     | 0 => m0
+     | p.+1 => (plus m0 p).+1
+     end)
+with
+| 0 => @erefl nat
+| n0.+1 => fun m0 : nat => erefl (plus m0 n0).+1
+end m.
+
+Definition plus_rect :
+forall (m : nat) (P : nat -> nat -> Type),
+       (forall n : nat, n = 0 -> P 0 m) ->
+       (forall n p : nat,
+        n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) ->
+       forall n : nat, P n (plus m n)
+:=
+fun (m : nat) (P : nat -> nat -> Type)
+  (f0 : forall n : nat, n = 0 -> P 0 m)
+  (f : forall n p : nat,
+       n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) =>
+fix plus0 (n : nat) : P n (plus m n) :=
+  eq_rect_r [eta P n]
+    (let f1 := f0 n in
+     let f2 := f n in
+     match
+       n as n0
+       return
+         (n = n0 ->
+          (forall p : nat,
+           n0 = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) ->
+          (n0 = 0 -> P 0 m) ->
+          P n0 match n0 with
+               | 0 => m
+               | p.+1 => (plus m p).+1
+               end)
+     with
+     | 0 =>
+         fun (_ : n = 0)
+           (_ : forall p : nat,
+                0 = p.+1 ->
+                P p (plus m p) -> P p.+1 (plus m p).+1)
+           (f4 : 0 = 0 -> P 0 m) => unkeyed (f4 (erefl 0))
+     | n0.+1 =>
+         fun (_ : n = n0.+1)
+           (f3 : forall p : nat,
+                 n0.+1 = p.+1 ->
+                 P p (plus m p) -> P p.+1 (plus m p).+1)
+           (_ : n0.+1 = 0 -> P 0 m) =>
+         let f5 :=
+           let p := n0 in
+           let H := erefl n0.+1 : n0.+1 = p.+1 in f3 p H in
+         unkeyed (let Hrec := plus0 n0 in f5 Hrec)
+     end (erefl n) f2 f1) (plus_equation m n).
+
+Definition plus_ind := plus_rect.
+
+Lemma exF x y z: plus (plus x y) z = plus x (plus y z).
+elim/plus_ind: z / (plus _ z).
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: (plus _ z).
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: {z}(plus _ z).
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: {z}_.
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: z / _.
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+ done.
+by move=> _ p _ ->.
+Qed.
+
+(* BUG elim-False *)
+Lemma testeF : False -> 1 = 0.
+Proof. by elim. Qed.
diff --git a/test-suite/ssr/elim2.v b/test-suite/ssr/elim2.v
new file mode 100644
index 000000000..c7c20d8f8
--- /dev/null
+++ b/test-suite/ssr/elim2.v
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+(* div fintype finfun path bigop. *)
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
+  let s := \big[op/idx]_(i <- r | P i) F i in
+  K s * K' s -> K' s.
+Proof. by move=> /= [_]. Qed.
+Arguments big_load [R] K [K' idx op I r P F].
+
+Section Elim1.
+
+Variables (R : Type) (K : R -> Type) (f : R -> R).
+Variables (idx : R) (op op' : R -> R -> R).
+
+Hypothesis Kid : K idx.
+
+Ltac ASSERT1 := match goal with |- (K idx) => myadmit end.
+Ltac ASSERT2 K := match goal with |- (forall x1 : R, R ->
+    forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => myadmit end.
+
+
+Lemma big_rec I r (P : pred I) F
+    (Kop : forall i x, P i -> K x -> K (op (F i) x)) :
+  K (\big[op/idx]_(i <- r | P i) F i).
+Proof.
+elim/big_ind2: {-}_.
+  ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
+elim/big_ind2: _ / {-}_.
+  ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
+
+elim/big_rec2: (\big[op/idx]_(i <- r | P i) op idx (F i))
+  / (\big[op/idx]_(i <- r | P i) F i).
+  ASSERT1. match goal with |- (forall i : I, R -> forall y2 : R, is_true (P i) -> K y2 -> K (op (F i) y2)) => myadmit end. Undo 3.
+
+elim/(big_load (phantom R)): _.
+  Undo.
+
+Fail elim/big_rec2: {2}_.
+
+elim/big_rec2: (\big[op/idx]_(i <- r | P i) F i)
+  / {1}(\big[op/idx]_(i <- r | P i) F i).
+  Undo.
+
+elim/(big_load (phantom R)): _.
+Undo.
+
+Fail elim/big_rec2: _ / {2}(\big[op/idx]_(i <- r | P i) F i).
+Admitted.
+
+Definition morecomplexthannecessary A (P : A -> A -> Prop) x y := P x y.
+
+Lemma grab A (P : A -> A -> Prop) n m : (n = m) -> (P n n) -> morecomplexthannecessary A P n m.
+by move->.
+Qed.
+
+Goal forall n m, m + (n + m) = m + (n * 1 + m).
+Proof. move=> n m; elim/grab : (_ * _) / {1}n => //; exact: muln1. Qed.
+
+End Elim1.
diff --git a/test-suite/ssr/elim_pattern.v b/test-suite/ssr/elim_pattern.v
new file mode 100644
index 000000000..ef4658287
--- /dev/null
+++ b/test-suite/ssr/elim_pattern.v
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1).
+case: (X in _ = X) / eqP => _.
+match goal with |- (x == x) = true => myadmit end.
+match goal with |- (x == x) = false => myadmit end.
+Qed.
+
+Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1).
+elim: (x in RHS).
+match goal with |- (x == x) = _ => myadmit end.
+match goal with |- forall n, (x == x) = _ -> (x == x) = _ => myadmit end.
+Qed.
diff --git a/test-suite/ssr/first_n.v b/test-suite/ssr/first_n.v
new file mode 100644
index 000000000..4971add91
--- /dev/null
+++ b/test-suite/ssr/first_n.v
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+
+Lemma test : False -> (bool -> False -> True -> True) -> True.
+move=> F; let w := constr:(2) in apply; last w first.
+- by apply: F.
+- by apply: I.
+- by apply: true.
+Qed.
diff --git a/test-suite/ssr/gen_have.v b/test-suite/ssr/gen_have.v
new file mode 100644
index 000000000..249e006f9
--- /dev/null
+++ b/test-suite/ssr/gen_have.v
@@ -0,0 +1,174 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Axiom P : nat -> Prop.
+Lemma clear_test (b1 b2 : bool) : b2 = b2.
+Proof.
+(* wlog gH : (b3 := b2) / b2 = b3. myadmit. *)
+gen have {b1} H, gH : (b3 := b2) (w := erefl 3) / b2 = b3.
+  myadmit.
+Fail exact (H b1).
+exact (H b2 (erefl _)).
+Qed.
+
+
+Lemma test1 n (ngt0 : 0 < n) : P n.
+gen have lt2le, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0).
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+Check (lt2le : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+Check (H1 : 0 <= n).
+Check (H2 : n != 0).
+myadmit.
+Qed.
+
+Lemma test2 n (ngt0 : 0 < n) : P n.
+gen have _, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0).
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+lazymatch goal with
+ | lt2le : forall n : nat, is_true(0 < n) -> is_true((0 <= n) && (n != 0))
+    |- _ => fail "not cleared"
+ | _ => idtac end.
+Check (H1 : 0 <= n).
+Check (H2 : n != 0).
+myadmit.
+Qed.
+
+Lemma test3 n (ngt0 : 0 < n) : P n.
+gen have H : n ngt0 / (0 <= n) && (n != 0).
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test4 n (ngt0 : 0 < n) : P n.
+gen have : n ngt0 / (0 <= n) && (n != 0).
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+move=> H.
+Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test4bis n (ngt0 : 0 < n) : P n.
+wlog suff : n ngt0 / (0 <= n) && (n != 0); last first.
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+move=> H.
+Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test5 n (ngt0 : 0 < n) : P n.
+Fail gen have : / (0 <= n) && (n != 0).
+Abort.
+
+Lemma test6 n (ngt0 : 0 < n) : P n.
+gen have : n ngt0 / (0 <= n) && (n != 0) by myadmit.
+Abort.
+
+Lemma test7 n (ngt0 : 0 < n) : P n.
+Fail gen have : n / (0 <= n) && (n != 0).
+Abort.
+
+Lemma test3wlog2 n (ngt0 : 0 < n) : P n.
+gen have H : (m := n) ngt0 / (0 <= m) && (m != 0).
+  match goal with
+    ngt0 : is_true(0 < m) |- is_true((0 <= m) && (m != 0)) => myadmit end.
+Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test3wlog3 n (ngt0 : 0 < n) : P n.
+gen have H : {n} (m := n) (n := 0) ngt0 / (0 <= m) && (m != n).
+  match goal with
+    ngt0 : is_true(n < m) |- is_true((0 <= m) && (m != n)) => myadmit end.
+Check (H : forall m n : nat, n < m -> (0 <= m) && (m != n)).
+myadmit.
+Qed.
+
+Lemma testw1 n (ngt0 : 0 < n) : n <= 0.
+wlog H : (z := 0) (m := n) ngt0 / m != 0.
+  match goal with
+    |- (forall z m,
+          is_true(z < m) -> is_true(m != 0) -> is_true(m <= z)) ->
+       is_true(n <= 0) => myadmit end.
+Check(n : nat).
+Check(m : nat).
+Check(z : nat).
+Check(ngt0 : z < m).
+Check(H : m != 0).
+myadmit.
+Qed.
+
+Lemma testw2 n (ngt0 : 0 < n) : n <= 0.
+wlog H : (m := n) (z := (X in n <= X)) ngt0 / m != z.
+  match goal with
+    |- (forall m z : nat,
+          is_true(0 < m) -> is_true(m != z) -> is_true(m <= z)) ->
+            is_true(n <= 0)   => idtac end.
+Restart.
+wlog H : (m := n) (one := (X in X <= _)) ngt0 / m != one.
+  match goal with
+    |- (forall m one : nat,
+          is_true(one <= m) -> is_true(m != one) -> is_true(m <= 0)) ->
+            is_true(n <= 0)   => idtac end.
+Restart.
+wlog H : {n} (m := n) (z := (X in _ <= X)) ngt0 / m != z.
+  match goal with
+    |- (forall m z : nat,
+          is_true(0 < z) -> is_true(m != z) -> is_true(m <= 0)) ->
+            is_true(n <= 0)   => idtac end.
+  myadmit.
+Fail Check n.
+myadmit.
+Qed.
+
+Section Test.
+Variable x : nat.
+Definition addx y := y + x.
+
+Lemma testw3 (m n : nat) (ngt0 : 0 < n) : n <= addx x.
+wlog H : (n0 := n) (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y.
+  myadmit.
+myadmit.
+Qed.
+
+
+Definition twox := x + x.
+Definition bis := twox.
+
+Lemma testw3x n (ngt0 : 0 < n) : n + x <= twox.
+wlog H : (y := x) (@twoy := (X in _ <= X)) / twoy = 2 * y.
+  match goal with
+    |- (forall y : nat,
+         let twoy := y + y in
+         twoy = 2 * y -> is_true(n + y <= twoy)) ->
+       is_true(n + x <= twox) => myadmit end.
+Restart.
+wlog H : (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y.
+  match goal with
+    |- (forall y : nat,
+         let twoy := twox in
+         twoy = 2 * y -> is_true(n + y <= twoy)) ->
+       is_true(n + x <= twox) => myadmit end.
+myadmit.
+Qed.
+
+End Test.
+
+Lemma test_in n k (def_k : k = 0) (ngtk : k < n) : P n.
+rewrite -(add0n n) in {def_k k ngtk} (m := k) (def_m := def_k) (ngtm := ngtk).
+rewrite def_m add0n in {ngtm} (e := erefl 0 ) (ngt0 := ngtm) => {def_m}.
+myadmit.
+Qed.
diff --git a/test-suite/ssr/gen_pattern.v b/test-suite/ssr/gen_pattern.v
new file mode 100644
index 000000000..c0592e884
--- /dev/null
+++ b/test-suite/ssr/gen_pattern.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Notation "( a 'in' c )" := (a + c) (only parsing) : myscope.
+Delimit Scope myscope with myscope.
+
+Notation "( a 'in' c )" := (a + c) (only parsing).
+
+Lemma foo x y : x + x.+1 = x.+1 + y.
+move: {x} (x.+1) {1}x y (x.+1 in RHS).
+  match goal with |- forall a b c d, b + a = d + c => idtac end.
+Admitted.
+
+Lemma bar x y : x + x.+1 = x.+1 + y.
+move E: ((x.+1 in y)) => w.
+  match goal with |- x + x.+1 = w => rewrite -{w}E end.
+move E: (x.+1 in y)%myscope => w.
+  match goal with |- x + x.+1 = w => rewrite -{w}E end.
+move E: ((x + y).+1 as RHS) => w.
+  match goal with |- x + x.+1 = w => rewrite -{}E -addSn end.
+Admitted.
diff --git a/test-suite/ssr/have_TC.v b/test-suite/ssr/have_TC.v
new file mode 100644
index 000000000..b3a26ed2c
--- /dev/null
+++ b/test-suite/ssr/have_TC.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Class foo (T : Type) := { n : nat }.
+Instance five : foo nat := {| n := 5 |}.
+
+Definition bar T {f : foo T} m : Prop :=
+  @n _ f = m.
+
+Eval compute in (bar nat 7).
+
+Lemma a : True.
+set toto := bar _ 8.
+have titi : bar _ 5.
+  reflexivity.
+have titi2 : bar _ 5 := .
+  Fail reflexivity.
+  by myadmit.
+have totoc (H : bar _ 5) : 3 = 3 := eq_refl.
+move/totoc: nat => _.
+exact I.
+Qed.
+
+Set SsrHave NoTCResolution.
+
+Lemma a' : True.
+set toto := bar _ 8.
+have titi : bar _ 5.
+  Fail reflexivity.
+  by myadmit.
+have titi2 : bar _ 5 := .
+  Fail reflexivity.
+  by myadmit.
+have totoc (H : bar _ 5) : 3 = 3 := eq_refl.
+move/totoc: nat => _.
+exact I.
+Qed.
diff --git a/test-suite/ssr/have_transp.v b/test-suite/ssr/have_transp.v
new file mode 100644
index 000000000..1c998da71
--- /dev/null
+++ b/test-suite/ssr/have_transp.v
@@ -0,0 +1,48 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+
+
+Lemma test1 n : n >= 0.
+Proof.
+have [:s1] @h m : 'I_(n+m).+1.
+  apply: Sub 0 _.
+  abstract: s1 m.
+  by auto.
+cut (forall m, 0 < (n+m).+1); last assumption.
+rewrite [_ 1 _]/= in s1 h *.
+by [].
+Qed.
+
+Lemma test2 n : n >= 0.
+Proof.
+have [:s1] @h m : 'I_(n+m).+1 := Sub 0 (s1 m).
+  move=> m; reflexivity.
+cut (forall m, 0 < (n+m).+1); last assumption.
+by [].
+Qed.
+
+Lemma test3 n : n >= 0.
+Proof.
+Fail have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0 (s1 m)); auto.
+have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract: s1 m; auto.
+cut (forall m, 0 < (n+m).+1); last assumption.
+by [].
+Qed.
+
+Lemma test4 n : n >= 0.
+Proof.
+have @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract auto.
+by [].
+Qed.
diff --git a/test-suite/ssr/have_view_idiom.v b/test-suite/ssr/have_view_idiom.v
new file mode 100644
index 000000000..3d6c9d980
--- /dev/null
+++ b/test-suite/ssr/have_view_idiom.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+
+Lemma test (a b : bool) (pab : a && b) : b.
+have {pab} /= /andP [pa -> //] /= : true && (a && b) := pab.
+Qed.
diff --git a/test-suite/ssr/havesuff.v b/test-suite/ssr/havesuff.v
new file mode 100644
index 000000000..aa1f71879
--- /dev/null
+++ b/test-suite/ssr/havesuff.v
@@ -0,0 +1,85 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+
+Variables P G : Prop.
+
+Lemma test1 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suff {pg} H : P.
+  match goal with |- P -> G => move=> _; exact: pg p | _ => fail end.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Lemma test2 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suffices {pg} H : P.
+  match goal with |- P -> G => move=> _; exact: pg p | _ => fail end.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Lemma test3 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suff have {pg} H : P.
+  match goal with H : P |- G => exact: pg H | _ => fail end.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+
+Lemma test4 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suffices have {pg} H: P.
+  match goal with H : P |- G => exact: pg H | _ => fail end.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+
+(*
+Lemma test5 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suff have {pg} H : P := pg H.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+*)
+
+(*
+Lemma test6 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suff have {pg} H := pg H.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+*)
+
+Lemma test7 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suff {pg} H : P := pg.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Lemma test8 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suff {pg} H := pg.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Goal forall x y : bool, x = y -> x = y.
+move=> x y E.
+by have {x E} -> : x = y by [].
+Qed.
diff --git a/test-suite/ssr/if_isnt.v b/test-suite/ssr/if_isnt.v
new file mode 100644
index 000000000..b8f6b7739
--- /dev/null
+++ b/test-suite/ssr/if_isnt.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+
+Definition unopt (x : option bool) :=
+  if x isn't Some x then false else x.
+
+Lemma test1 : unopt None = false /\
+              unopt (Some false) = false /\
+              unopt (Some true) = true.
+Proof. by auto. Qed.
diff --git a/test-suite/ssr/intro_beta.v b/test-suite/ssr/intro_beta.v
new file mode 100644
index 000000000..8a164bd80
--- /dev/null
+++ b/test-suite/ssr/intro_beta.v
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+
+Axiom T : Type.
+
+Definition C (P : T -> Prop) := forall x, P x.
+
+Axiom P : T -> T -> Prop.
+
+Lemma foo : C (fun x => forall y, let z := x in P y x).
+move=> a b.
+match goal with |- (let y := _ in _) => idtac end.
+Admitted.
diff --git a/test-suite/ssr/intro_noop.v b/test-suite/ssr/intro_noop.v
new file mode 100644
index 000000000..fdc85173a
--- /dev/null
+++ b/test-suite/ssr/intro_noop.v
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Lemma v : True -> bool -> bool. Proof. by []. Qed.
+
+Reserved Notation " a -/ b " (at level 0).
+Reserved Notation " a -// b " (at level 0).
+Reserved Notation " a -/= b " (at level 0).
+Reserved Notation " a -//= b " (at level 0).
+
+Lemma test : forall a b c, a || b || c.
+Proof.
+move=> ---a--- - -/=- -//- -/=- -//=- b [|-].
+move: {-}a => /v/v-H; have _ := H I I.
+Fail move: {-}a {H} => /v-/v-H.
+have - -> : a = (id a) by [].
+have --> : a = (id a) by [].
+have - - _ : a = (id a) by [].
+have -{1}-> : a = (id a) by [].
+  by myadmit.
+move: a.
+case: b => -[] //.
+by myadmit.
+Qed.
diff --git a/test-suite/ssr/ipatalternation.v b/test-suite/ssr/ipatalternation.v
new file mode 100644
index 000000000..6aa9a954c
--- /dev/null
+++ b/test-suite/ssr/ipatalternation.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+
+Lemma test1 : Prop -> Prop -> Prop -> Prop -> Prop -> True = False -> Prop -> True \/ True.
+by move=> A /= /= /= B C {A} {B} ? _ {C} {1}-> *; right.
+Qed.
diff --git a/test-suite/ssr/ltac_have.v b/test-suite/ssr/ltac_have.v
new file mode 100644
index 000000000..380e52af4
--- /dev/null
+++ b/test-suite/ssr/ltac_have.v
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Ltac SUFF1 h t := suff h x (p := x < 0) : t.
+Ltac SUFF2 h t := suff h x (p := x < 0) : t by apply h.
+Ltac HAVE1 h t u := have h x (p := x < 0) : t := u.
+Ltac HAVE2 h t := have h x (p := x < 0) : t by [].
+Ltac HAVE3 h t := have h x (p := x < 0) : t.
+Ltac HAVES h t := have suff h : t.
+Ltac SUFFH h t := suff have h : t.
+
+Lemma foo z : z < 0.
+SUFF1 h1 (z+1 < 0).
+Undo.
+SUFF2 h2 (z < 0).
+Undo.
+HAVE1 h3 (z = z) (refl_equal z).
+Undo.
+HAVE2 h4 (z = z).
+Undo.
+HAVE3 h5 (z < 0).
+Undo.
+HAVES h6 (z < 1).
+Undo.
+SUFFH h7 (z < 1).
+Undo.
+Admitted.
diff --git a/test-suite/ssr/ltac_in.v b/test-suite/ssr/ltac_in.v
new file mode 100644
index 000000000..bcdf96dde
--- /dev/null
+++ b/test-suite/ssr/ltac_in.v
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
+(* error 1 *)
+
+Ltac subst1 H := move: H; rewrite {1} addnC; move => H.
+Ltac subst2 H := rewrite addnC in H.
+
+Goal ( forall a b: nat, b+a = 0 -> b+a=0).
+Proof. move=> a b hyp. subst1 hyp. subst2 hyp. done. Qed.
diff --git a/test-suite/ssr/move_after.v b/test-suite/ssr/move_after.v
new file mode 100644
index 000000000..a7a9afea0
--- /dev/null
+++ b/test-suite/ssr/move_after.v
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+
+Goal True -> True -> True.
+move=> H1 H2.
+move H1 after H2.
+Admitted.
diff --git a/test-suite/ssr/multiview.v b/test-suite/ssr/multiview.v
new file mode 100644
index 000000000..f4e717b38
--- /dev/null
+++ b/test-suite/ssr/multiview.v
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Goal forall m n p, n <= p -> m <= n -> m <= p.
+by move=> m n p le_n_p /leq_trans; apply.
+Undo 1.
+by move=> m n p le_n_p /leq_trans /(_ le_n_p) le_m_p; exact: le_m_p.
+Undo 1.
+by move=> m n p le_n_p /leq_trans ->.
+Qed.
+
+Goal forall P Q X : Prop, Q -> (True -> X -> Q = P) -> X -> P.
+by move=> P Q X q V /V <-.
+Qed.
+
+Lemma test0: forall a b, a && a && b -> b.
+by move=> a b; repeat move=> /andP []; move=> *.
+Qed.
+
+Lemma test1 : forall a b, a && b -> b.
+by move=> a b /andP /andP /andP [] //.
+Qed.
+
+Lemma test2 : forall a b, a && b -> b.
+by move=> a b /andP /andP /(@andP a) [] //.
+Qed.
+
+Lemma test3 : forall a b, a && (b && b) -> b.
+by move=> a b /andP [_ /andP [_ //]].
+Qed.
+
+Lemma test4:  forall a b, a && b = b && a.
+by move=> a b; apply/andP/andP=> ?; apply/andP/andP/andP; rewrite andbC; apply/andP.
+Qed.
+
+Lemma test5:  forall C I A O, (True -> O) -> (O -> A) -> (True -> A -> I) -> (I -> C) -> C.
+by move=> c i a o O A I C; apply/C/I/A/O.
+Qed.
+
+Lemma test6:  forall A B, (A -> B) -> A -> B.
+move=> A B A_to_B a; move/A_to_B in a; exact: a.
+Qed.
+
+Lemma test7:  forall A B, (A -> B) -> A -> B.
+move=> A B A_to_B a; apply A_to_B in a; exact: a.
+Qed.
diff --git a/test-suite/ssr/occarrow.v b/test-suite/ssr/occarrow.v
new file mode 100644
index 000000000..49af7ae08
--- /dev/null
+++ b/test-suite/ssr/occarrow.v
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : forall n m : nat, n = m -> m * m + n * n = n * n + n * n.
+move=> n m E; have [{2}-> _] : n * n = m * n /\ True by move: E => {1}<-.
+by move: E => {3}->.
+Qed.
+
+Lemma test2 : forall n m : nat, True /\ (n = m -> n * n = n * m).
+by move=> n m; constructor=> [|{2}->].
+Qed.
diff --git a/test-suite/ssr/patnoX.v b/test-suite/ssr/patnoX.v
new file mode 100644
index 000000000..d69f03ac3
--- /dev/null
+++ b/test-suite/ssr/patnoX.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Goal forall x, x && true = x.
+move=> x.
+Fail (rewrite [X in _ && _]andbT).
+Abort.
diff --git a/test-suite/ssr/pattern.v b/test-suite/ssr/pattern.v
new file mode 100644
index 000000000..396f4f032
--- /dev/null
+++ b/test-suite/ssr/pattern.v
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import ssrmatching.
+
+(*Set Debug SsrMatching.*)
+
+Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) :=
+  let name := fresh in
+  let def_name := fresh in
+  ssrpattern pat;
+  intro name;
+  pose proof (refl_equal name) as def_name;
+  unfold name at 1 in def_name;
+  t def_name;
+  [ rewrite <- def_name | idtac.. ];
+  clear name def_name.
+
+Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4.
+Proof.
+at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place).
+- reflexivity.
+- trivial.
+- trivial.
+Qed.
diff --git a/test-suite/ssr/primproj.v b/test-suite/ssr/primproj.v
new file mode 100644
index 000000000..cf61eb436
--- /dev/null
+++ b/test-suite/ssr/primproj.v
@@ -0,0 +1,164 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+
+
+Require Import Setoid.
+Set Primitive Projections.
+
+
+Module CoqBug.
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Variable alias : forall A, foo A -> A.
+
+Parameter e : @foo_car = alias.
+
+Goal foo_car _ bar = alias _ bar.
+Proof.
+(* Coq equally fails *)
+Fail rewrite -> e.
+Fail rewrite e at 1.
+Fail setoid_rewrite e.
+Fail setoid_rewrite e at 1.
+Set Keyed Unification.
+Fail rewrite -> e.
+Fail rewrite e at 1.
+Fail setoid_rewrite e.
+Fail setoid_rewrite e at 1.
+Admitted.
+
+End CoqBug.
+
+(* ----------------------------------------------- *)
+Require Import ssreflect.
+
+Set Primitive Projections.
+
+Module T1.
+
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Goal foo_car _ bar = 10.
+Proof.
+match goal with
+| |- foo_car _ bar = 10 => idtac
+end.
+rewrite /foo_car.
+(*
+Fail match goal with
+| |- foo_car _ bar = 10 => idtac
+end.
+*)
+Admitted.
+
+End T1.
+
+
+Module T2.
+
+Record foo {A} := Foo { foo_car : A }.
+
+Definition bar : foo := Foo nat 10.
+
+Goal foo_car bar = 10.
+match goal with
+| |- foo_car bar = 10 => idtac
+end.
+rewrite /foo_car.
+(*
+Fail match goal with
+| |- foo_car bar = 10 => idtac
+end.
+*)
+Admitted.
+
+End T2.
+
+
+Module T3.
+
+Record foo {A} := Foo { foo_car : A }.
+
+Definition bar : foo := Foo nat 10.
+
+Goal foo_car bar = 10.
+Proof.
+rewrite -[foo_car _]/(id _).
+match goal with |- id _ = 10 => idtac end.
+Admitted.
+
+Goal foo_car bar = 10.
+Proof.
+set x := foo_car _.
+match goal with |- x = 10 => idtac end.
+Admitted.
+
+End T3.
+
+Module T4.
+
+Inductive seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+Arguments unseal {_ _} _.
+Arguments seal_eq {_ _} _.
+
+Record uPred : Type := IProp { uPred_holds :> Prop }.
+
+Definition uPred_or_def (P Q : uPred) : uPred :=
+  {| uPred_holds := P \/ Q |}.
+Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed.
+Definition uPred_or := unseal uPred_or_aux.
+Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux.
+
+Lemma foobar (P1 P2 Q : uPred) :
+  (P1 <-> P2) -> (uPred_or P1 Q) <-> (uPred_or P2 Q).
+Proof.
+  rewrite uPred_or_eq. (* This fails. *)
+Admitted.
+
+End T4.
+
+
+Module DesignFlaw.
+
+Record foo A := Foo { foo_car : A }.
+Definition bar : foo _ := Foo nat 10.
+
+Definition app (f : foo nat -> nat) x := f x.
+
+Goal app (foo_car _) bar = 10.
+Proof.
+unfold app.  (* mkApp should produce a Proj *)
+Fail set x := (foo_car _ _).
+Admitted.
+
+End DesignFlaw.
+
+
+Module Bug.
+
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Variable alias : forall A, foo A -> A.
+
+Parameter e : @foo_car = alias.
+
+Goal foo_car _ bar = alias _ bar.
+Proof.
+Fail rewrite e.  (* Issue: #86 *)
+Admitted.
+
+End Bug.
diff --git a/test-suite/ssr/rewpatterns.v b/test-suite/ssr/rewpatterns.v
new file mode 100644
index 000000000..f7993f402
--- /dev/null
+++ b/test-suite/ssr/rewpatterns.v
@@ -0,0 +1,146 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+
+Require Import ssreflect.
+Require Import ssrbool ssrfun TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1).
+by move=> x y f; rewrite [_.+1](addnC x.+1).
+Qed.
+
+Lemma test2 : forall x y f, x + y + f (y + x) + f (y + x) = x + y + f (y + x) + f (x + y).
+by move=> x y f; rewrite {2}[in f _]addnC.
+Qed.
+
+Lemma test2' : forall x y f, true && f (x * (y + x)) = true && f(x * (x + y)).
+by move=> x y f; rewrite [in f _](addnC y).
+Qed.
+
+Lemma test2'' : forall x y f, f (y + x) + f(y + x) + f(y + x)  = f(x + y) + f(y + x) + f(x + y).
+by move=> x y f; rewrite {1 3}[in f _](addnC y).
+Qed.
+
+(* patterns catching bound vars not supported *)
+Lemma test2_1 : forall x y f, true && (let z := x in f (z * (y + x))) = true && f(x * (x + y)).
+by move=> x y f; rewrite [in f _](addnC x). (* put y when bound var will be OK *)
+Qed.
+
+Lemma test3 : forall x y f, x + f (x + y) (f (y + x) x) = x + f (x + y) (f (x + y) x).
+by move=> x y f; rewrite [in X in (f _ X)](addnC y).
+Qed.
+
+Lemma test3' : forall x y f, x = y -> x + f (x + x) x + f (x + x) x =
+                                      x + f (x + y) x + f (y + x) x.
+by move=> x y f E; rewrite {2 3}[in X in (f X _)]E.
+Qed.
+
+Lemma test3'' : forall x y f, x = y -> x + f (x + y) x + f (x + y) x =
+                                       x + f (x + y) x + f (y + y) x.
+by move=> x y f E; rewrite {2}[in X in (f X _)]E.
+Qed.
+
+Lemma test4 : forall x y f, x = y -> x + f (fun _ : nat => x + x) x + f (fun _ => x + x) x =
+                                     x + f (fun _       => x + y) x + f (fun _ => y + x) x.
+by move=> x y f E; rewrite {2 3}[in X in (f X _)]E.
+Qed.
+
+Lemma test4' : forall x y f, x = y -> x + f (fun _ _ _ : nat => x + x) x =
+                                      x + f (fun _ _ _       => x + y) x.
+by move=> x y f E; rewrite {2}[in X in (f X _)]E.
+Qed.
+
+Lemma test5 : forall x y f, x = y -> x + f (y + x) x + f (y + x) x =
+                                     x + f (x + y) x + f (y + x) x.
+by move=> x y f E; rewrite {1}[X in (f X _)]addnC.
+Qed.
+
+Lemma test3''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) =
+                                        x + f (x + y) x + f (y + y) (x + y).
+by move=> x y f E; rewrite {1}[in X in (f X X)]E.
+Qed.
+
+Lemma test3'''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) =
+                                         x + f (x + y) x + f (y + y) (y + y).
+by move=> x y f E; rewrite [in X in (f X X)]E.
+Qed.
+
+Lemma test3x : forall x y f, y+y = x+y -> x + f (x + y) x + f (x + y) (x + y) =
+                                         x + f (x + y) x + f (y + y) (y + y).
+by move=> x y f E; rewrite -[X in (f X X)]E.
+Qed.
+
+Lemma test6 : forall x y (f : nat -> nat), f (x + y).+1 = f (y.+1 + x).
+by move=> x y f; rewrite [(x + y) in X in (f X)]addnC.
+Qed.
+
+Lemma test7 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1).
+by move=> x y f; rewrite [(x.+1 + y) as X in (f X)]addnC.
+Qed.
+
+Lemma manual x y z (f : nat -> nat -> nat) : (x + y).+1 + f (x.+1 + y) (z + (x + y).+1) = 0.
+Proof.
+rewrite [in f _]addSn.
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 => idtac end.
+rewrite -[X in _ = X]addn0.
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + 0 => idtac end.
+rewrite -{2}[in X in _ = X](addn0 0).
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + (0 + 0) => idtac end.
+rewrite [_.+1 in X in f _ X](addnC x.+1).
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (y + x.+1)) = 0 + (0 + 0) => idtac end.
+rewrite [x.+1 + y as X in f X _]addnC.
+match goal with |- (x + y).+1 + f (y + x.+1) (z + (y + x.+1)) = 0 + (0 + 0) => idtac end.
+Admitted.
+
+Goal (exists x : 'I_3, x > 0).
+apply: (ex_intro _ (@Ordinal _ 2 _)).
+Admitted.
+
+Goal (forall y, 1 < y < 2 -> exists x : 'I_3, x > 0).
+move=> y; case/andP=> y_gt1 y_lt2; apply: (ex_intro _ (@Ordinal _ y _)).
+ by apply: leq_trans y_lt2 _.
+by move=> y_lt3; apply: leq_trans _ y_gt1.
+Qed.
+
+Goal (forall x y : nat, forall P : nat -> Prop, x = y -> True).
+move=> x y P E.
+have: P x -> P y by suff: x = y by move=> ?; congr (P _).
+Admitted.
+
+Goal forall a : bool, a -> true && a || false && a.
+by move=> a ?; rewrite [true && _]/= [_ && a]/= orbC [_ || _]//=.
+Qed.
+
+Goal forall a : bool, a -> true && a || false && a.
+by move=> a ?; rewrite [X in X || _]/= [X in _ || X]/= orbC [false && a as X in X || _]//=.
+Qed.
+
+Variable a : bool.
+Definition f x := x || a.
+Definition g x := f x.
+
+Goal a -> g false.
+by move=> Ha; rewrite [g _]/f orbC Ha.
+Qed.
+
+Goal a -> g false || g false.
+move=> Ha; rewrite {2}[g _]/f orbC Ha.
+match goal with |- (is_true (false || true || g false)) => done end.
+Qed.
+
+Goal a -> (a && a || true && a) && true.
+by move=> Ha; rewrite -[_ || _]/(g _) andbC /= Ha [g _]/f.
+Qed.
+
+Goal a -> (a || a) && true.
+by move=> Ha; rewrite -[in _ || _]/(f _) Ha andbC /f.
+Qed.
diff --git a/test-suite/ssr/set_lamda.v b/test-suite/ssr/set_lamda.v
new file mode 100644
index 000000000..a012ec680
--- /dev/null
+++ b/test-suite/ssr/set_lamda.v
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool ssrfun.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
+(* error 2 *)
+
+Goal (exists f: Set -> nat, f nat = 0).
+Proof. set (f:= fun  _:Set =>0). by exists f. Qed.
+
+Goal (exists f: Set -> nat, f nat = 0).
+Proof. set f := (fun  _:Set =>0). by exists f. Qed.
diff --git a/test-suite/ssr/set_pattern.v b/test-suite/ssr/set_pattern.v
new file mode 100644
index 000000000..3ce75e879
--- /dev/null
+++ b/test-suite/ssr/set_pattern.v
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Ltac T1 x := match goal with |- _ => set t := (x in X in _ = X) end.
+Ltac T2 x := first [set t := (x in RHS)].
+Ltac T3 x := first [set t := (x in Y in _ = Y)|idtac].
+Ltac T4 x := set t := (x in RHS); idtac.
+Ltac T5 x := match goal with |- _ => set t := (x in RHS) | |- _ => idtac end.
+
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Open Scope nat_scope.
+
+Lemma foo x y : x.+1 = y + x.+1.
+set t := (_.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (x in _ = x). match goal with |- x.+1 = t => rewrite /t {t} end.
+set t := (x in X in _ = X).
+  match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (y + (1 + x) as X in _ = X).
+  match goal with |- x.+1 = t => rewrite /t addSn add0n {t} end.
+set t := x.+1. match goal with |- t = y + t => rewrite /t {t} end.
+set t := (x).+1. match goal with |- t = y + t => rewrite /t {t} end.
+set t := ((x).+1 in X in _ = X).
+  match goal with |- x.+1 = y + t => rewrite /t {t} end.
+set t := (x.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T1 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T2 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T3 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T4 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T5 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+rewrite [RHS]addnC.
+  match goal with |- x.+1 = x.+1 + y => rewrite -[RHS]addnC end.
+rewrite -[in RHS](@subnK 1 x.+1) //.
+  match goal with |- x.+1 = y + (x.+1 - 1 + 1) => rewrite subnK // end.
+have H : x.+1 = y by myadmit.
+set t := _.+1 in H |- *.
+  match goal with H : t = y |- t = y + t => rewrite /t {t} in H * end.
+set t := (_.+1 in X in _ + X) in H |- *.
+  match goal with H : x.+1 = y |- x.+1 = y + t => rewrite /t {t} in H * end.
+set t := 0. match goal with t := 0 |- x.+1 = y + x.+1 => clear t end.
+set t := y + _. match goal with |- x.+1 = t => rewrite /t {t} end.
+set t : nat := 0. clear t.
+set t : nat := (x in RHS).
+  match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t : nat := RHS. match goal with |- x.+1 = t => rewrite /t {t} end.
+(* set t := 0 + _. *)
+(* set t := (x).+1 in X in _ + X in H |-. *)
+(* set t := (x).+1 in X in _ = X.*)
+Admitted.
diff --git a/test-suite/ssr/ssrsyntax2.v b/test-suite/ssr/ssrsyntax2.v
new file mode 100644
index 000000000..af839fabd
--- /dev/null
+++ b/test-suite/ssr/ssrsyntax2.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import TestSuite.ssr_ssrsyntax1.
+Require Import Arith.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite plus_comm, plus_comm.
+split.
+Qed.
diff --git a/test-suite/ssr/tc.v b/test-suite/ssr/tc.v
new file mode 100644
index 000000000..ae4589ef3
--- /dev/null
+++ b/test-suite/ssr/tc.v
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+
+Class foo (A : Type) : Type := mkFoo { val : A }.
+Instance foo_pair {A B} {f1 : foo A} {f2 : foo B} : foo (A * B) | 2 :=
+  {| val := (@val _ f1, @val _ f2) |}.
+Instance foo_nat : foo nat | 3 := {| val := 0 |}.
+
+Definition id {A} (x : A) := x.
+Axiom E : forall A {f : foo A} (a : A), id a = (@val _ f).
+
+Lemma test (x : nat) : id true = true -> id x = 0.
+Proof.
+Fail move=> _; reflexivity.
+Timeout 2 rewrite E => _; reflexivity.
+Qed.
+
+Definition P {A} (x : A) : Prop := x = x.
+Axiom V : forall A {f : foo A} (x:A), P x -> P (id x).
+
+Lemma test1 (x : nat) : P x -> P (id x).
+Proof.
+move=> px.
+Timeout 2 Fail move/V: px.
+Timeout 2 move/V : (px) => _.
+move/(V nat) : px => H; exact H.
+Qed.
diff --git a/test-suite/ssr/typeof.v b/test-suite/ssr/typeof.v
new file mode 100644
index 000000000..ca121fdb3
--- /dev/null
+++ b/test-suite/ssr/typeof.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+
+Ltac mycut x :=
+  let tx := type of x in
+  cut tx.
+
+Lemma test : True.
+Proof.
+by mycut I=> [ x | ]; [ exact x | exact I ].
+Qed.
diff --git a/test-suite/ssr/unfold_Opaque.v b/test-suite/ssr/unfold_Opaque.v
new file mode 100644
index 000000000..7c2b51de4
--- /dev/null
+++ b/test-suite/ssr/unfold_Opaque.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import ssreflect.
+
+Definition x := 3.
+Opaque x.
+
+Goal x = 3.
+Fail rewrite /x.
+Admitted.
diff --git a/test-suite/ssr/unkeyed.v b/test-suite/ssr/unkeyed.v
new file mode 100644
index 000000000..710941c30
--- /dev/null
+++ b/test-suite/ssr/unkeyed.v
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
+Lemma test0 (a b : unit) f : a = f b.
+Proof. by rewrite !unitE.  Qed.
+
+Lemma phE T : all_equal_to (Phant T). Proof. by case. Qed.
+
+Lemma test1 (a b : phant nat) f : a = f b.
+Proof.  by rewrite !phE.  Qed.
+
+Lemma eq_phE (T : eqType) : all_equal_to (Phant T). Proof. by case. Qed.
+
+Lemma test2 (a b : phant bool) f : a = locked (f b).
+Proof. by rewrite !eq_phE. Qed.
diff --git a/test-suite/ssr/view_case.v b/test-suite/ssr/view_case.v
new file mode 100644
index 000000000..2721470c4
--- /dev/null
+++ b/test-suite/ssr/view_case.v
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Axiom P : forall T, seq T -> Prop.
+
+Goal (forall T (s : seq T), P _ s).
+move=> T s.
+elim: s => [| x /lastP [| s] IH].
+Admitted.
+
+Goal forall x : 'I_1, x = 0 :> nat.
+move=> /ord1 -> /=; exact: refl_equal.
+Qed.
+
+Goal forall x : 'I_1, x = 0 :> nat.
+move=> x.
+move=> /ord1 -> in x |- *.
+exact: refl_equal.
+Qed.
diff --git a/test-suite/ssr/wlog_suff.v b/test-suite/ssr/wlog_suff.v
new file mode 100644
index 000000000..43a8f3b8b
--- /dev/null
+++ b/test-suite/ssr/wlog_suff.v
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+
+Lemma test b : b || ~~b.
+wlog _ : b / b = true.
+  case: b; [ by apply | by rewrite orbC ].
+wlog suff: b /  b || ~~b.
+  by case: b.
+by case: b.
+Qed.
+
+Lemma test2 b c (H : c = b) : b || ~~b.
+wlog _ : b {c H} / b = true.
+  by case: b H.
+by case: b.
+Qed.
diff --git a/test-suite/ssr/wlogletin.v b/test-suite/ssr/wlogletin.v
new file mode 100644
index 000000000..64e1ea84f
--- /dev/null
+++ b/test-suite/ssr/wlogletin.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Variable T : Type.
+Variables P : T -> Prop.
+
+Definition f := fun x y : T => x.
+
+Lemma test1 : forall x y : T, P (f x y) -> P x.
+Proof.
+move=> x y; set fxy := f x y; move=> Pfxy.
+wlog H : @fxy Pfxy / P x.
+  match goal with |- (let fxy0 := f x y in P fxy0 -> P x -> P x) -> P x => by auto | _ => fail end.
+exact: H.
+Qed.
+
+Lemma test2 : forall x y : T, P (f x y) -> P x.
+Proof.
+move=> x y; set fxy := f x y; move=> Pfxy.
+wlog H : fxy Pfxy / P x.
+  match goal with |- (forall fxy, P fxy -> P x -> P x) -> P x => by auto | _ => fail end.
+exact: H.
+Qed.
+
+Lemma test3 : forall x y : T, P (f x y) -> P x.
+Proof.
+move=> x y; set fxy := f x y; move=> Pfxy.
+move: {1}@fxy (Pfxy) (Pfxy).
+match goal with |- (let fxy0 := f x y in P fxy0 -> P fxy -> P x) => by auto | _ => fail end.
+Qed.
+
+Lemma test4 : forall n m z: bool, n = z -> let x := n in x = m && n -> x = m && n.
+move=> n m z E x H.
+case: true.
+  by rewrite {1 2}E in (x) H |- *.
+by rewrite {1}E in x H |- *.
+Qed.
diff --git a/test-suite/ssr/wlong_intro.v b/test-suite/ssr/wlong_intro.v
new file mode 100644
index 000000000..dd80f0435
--- /dev/null
+++ b/test-suite/ssr/wlong_intro.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Goal (forall x y : nat, True).
+move=> x y.
+wlog suff: x y / x <= y.
+Admitted.