2 files changed, 27 insertions, 9 deletions
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index fc02cef100..329fa0ee81 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -427,19 +427,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;
-  unfold g;clear g.
-
+  (* 
+     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.
+\ No newline at end of file
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 0f996c65aa..d0fe1f9570 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -131,7 +131,7 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
   TacFun([Name(Id.of_string"t")],
   TacML(Loc.tag (tacname,
-  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None));
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
    TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"