From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 plugins/setoid_ring/Ring_tac.v | 42 +++++++++++++++++++++++++++++++++++-------
 1 file changed, 35 insertions(+), 7 deletions(-)

(limited to 'plugins/setoid_ring/Ring_tac.v')

diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index fc02cef1..e8efb362 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
 Set Implicit Arguments.
 Require Import Setoid.
 Require Import BinPos.
@@ -427,19 +437,37 @@ 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;
+  (* 
+     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;
+  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;
+  (* 
+     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;
+  clear H;rename H' into H;
   unfold g;clear g.
-
-- 
cgit v1.2.3