From 3c2ea907cd98bbd2c5c2b97bcf3cb5ae9a475e76 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 20 Oct 2004 09:25:54 +0000
Subject: The bug already closed in revision 1.90 was reintroduced again.
 Closed again.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6243 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index c58400d39e..cf0388543d 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -979,8 +979,9 @@ let int_add_relation id a aeq refl sym trans =
    } in
   let x_relation_class =
    let subst =
+    let len = List.length a_quantifiers_rev in
     Array.of_list
-     (Util.list_map_i (fun i _ -> mkRel (i + 2)) 1 a_quantifiers_rev) in
+     (Util.list_map_i (fun i _ -> mkRel (len - i + 2)) 0 a_quantifiers_rev) in
    cic_relation_class_of_X_relation
     (mkRel 2) (mkRel 1) (apply_to_relation subst aeq_rel) in
   let _ =
@@ -997,8 +998,9 @@ let int_add_relation id a aeq refl sym trans =
   let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in
   let xreflexive_relation_class =
    let subst =
+    let len = List.length a_quantifiers_rev in
     Array.of_list
-     (Util.list_map_i (fun i _ -> mkRel i) 1 a_quantifiers_rev)
+     (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 a_quantifiers_rev)
    in
     cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in
   let _ =
-- 
cgit v1.2.3