From 0dd691120e9480fdd9550462508b60609edc8427 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 16 Jul 2010 14:17:53 +0000
Subject: fixed bug #2316 (ring_simplify)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13284 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/Ring_tac.v | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index e3eb418ad1..d33e9a82a1 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.
-- 
cgit v1.2.3