From 11ab8eb6c7f6475de03c7ce258bf48d461d5892f Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Tue, 1 Aug 2017 00:07:12 +0200
Subject: solving b1859

---
 plugins/setoid_ring/Ring_tac.v | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index fc02cef100..d488ef140e 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -427,19 +427,23 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
   let t := type of H in
   let g := fresh "goal" in
   set (g:= G);
-  generalize H;clear H;
+  generalize H;
   ring_lookup (PackRing Ring_simplify) [] rl t;
-  intro H;
+  let H' := fresh "H" in
+  intro H';
+  move H' after H;
+  clear H;rename H' into H;
   unfold g;clear g.
 
-Tactic Notation
-  "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
+Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
   let G := Get_goal in
   let t := type of H in
   let g := fresh "goal" in
   set (g:= G);
-  generalize H;clear H;
+  generalize H;
   ring_lookup (PackRing Ring_simplify) [lH] rl t;
-  intro H;
-  unfold g;clear g.
-
+  let H' := fresh "H" in
+  intro H';
+  move H' after H;
+  clear H;rename H' into H;
+  unfold g;clear g.
\ No newline at end of file
-- 
cgit v1.2.3


From b4aba0a95493e7dd9f9bbfcaeade4015b697cd00 Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Tue, 1 Aug 2017 11:53:58 +0200
Subject: adding a comment to explain the change

---
 plugins/setoid_ring/Ring_tac.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index d488ef140e..329fa0ee81 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -429,6 +429,13 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
   set (g:= G);
   generalize H;
   ring_lookup (PackRing Ring_simplify) [] rl t;
+  (* 
+     Correction of bug 1859:
+     we want to leave H at its initial position
+     this is obtained by adding a copy of H (H'), 
+     move it just after H, remove H and finally 
+     rename H into H'
+   *)
   let H' := fresh "H" in
   intro H';
   move H' after H;
@@ -442,6 +449,13 @@ Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H
   set (g:= G);
   generalize H;
   ring_lookup (PackRing Ring_simplify) [lH] rl t;
+  (* 
+     Correction of bug 1859:
+     we want to leave H at its initial position
+     this is obtained by adding a copy of H (H'), 
+     move it just after H, remove H and finally 
+     rename H into H'
+   *)
   let H' := fresh "H" in
   intro H';
   move H' after H;
-- 
cgit v1.2.3


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