From 5da0ac62b272c7595da16222e8e9004dc4d459a9 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Mon, 18 Oct 2004 13:28:17 +0000
Subject: Bug fixed: relations quantified more than once where abstracted in
 the wrong order (and thus they were not accepted).

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

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index be49e06d0a..f147e569e7 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -637,7 +637,8 @@ let morphism_theory_id_of_morphism_proof_id id =
 
 (* apply_to_rels c [l1 ; ... ; ln] returns (c Rel1 ... reln) *)
 let apply_to_rels c l =
- applistc c (Util.list_map_i (fun i _ -> mkRel i) 1 l)
+ let len = List.length l in
+  applistc c (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 l)
 
 let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
  let env = Global.env() in
-- 
cgit v1.2.3