From 0b0411c56cac33ccd9474da4ae71d498355422b3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 15 Aug 2017 12:53:28 +0200
Subject: Adding a test for BZ#1859 as suggested by @tchajed.

---
 test-suite/bugs/closed/1859.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/bugs/closed/1859.v

diff --git a/test-suite/bugs/closed/1859.v b/test-suite/bugs/closed/1859.v
new file mode 100644
index 0000000000..43acfe4ba2
--- /dev/null
+++ b/test-suite/bugs/closed/1859.v
@@ -0,0 +1,20 @@
+Require Import Ring.
+Require Import ArithRing.
+
+Ltac ring_simplify_neq :=
+  match goal with
+  | [ H: ?X <> ?Y |- _ ] => progress ring_simplify X Y in H
+  end.
+
+Lemma toto : forall x y, x*1 <> y*1 -> y*1 <> x*1 -> x<>y.
+Proof.
+  intros.
+  ring_simplify_neq.
+  ring_simplify_neq.
+  (* make sure ring_simplify has simplified both hypotheses *)
+  match goal with
+  | [ H: context[_*1] |- _ ] => fail 1
+  | _ => idtac
+  end.
+  auto.
+Qed.
-- 
cgit v1.2.3