fixed bug #2316 (ring_simplify)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13284 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 4 deletions

diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index e3eb418ad..d33e9a82a 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -124,11 +124,11 @@ Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac :=
    - [SYN_tac term fv] reifies [term] given the list of atomic expressions
    - [LEMMA_tac fv kont] computes the correctness lemma and passes it to
        continuation kont
-   - [MAIN_tac H] process H which is the conclusion of the correctness
-       lemma instantiated with each reified term
+   - [MAIN_tac H] process H which is the conclusion of the correctness lemma
+       instantiated with each reified term
    - [fv] is the initial value of atomic expressions (to be completed by
        the reification of the terms
-   - [terms] the list (a constr of type list) of terms to reify ans process.
+   - [terms] the list (a constr of type list) of terms to reify and process.
  *)
 Ltac ReflexiveRewriteTactic
      FV_tac SYN_tac LEMMA_tac MAIN_tac fv terms :=
@@ -137,7 +137,12 @@ Ltac ReflexiveRewriteTactic
   let RW_tac lemma :=
      let fcons term CONT_tac :=
       let expr := SYN_tac term fv in
-      (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac) in
+      let main H :=
+        match type of H with
+        | (?req _ ?rhs) => change (req term rhs) in H
+        end;
+        MAIN_tac H in
+      (ApplyLemmaThenAndCont lemma expr main CONT_tac) in
      (* rewrite steps *)
      lazy_list_fold_right fcons ltac:(fun _=>idtac) terms in
   LEMMA_tac fv RW_tac.