diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 09:25:54 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 09:25:54 +0000 |
| commit | 3c2ea907cd98bbd2c5c2b97bcf3cb5ae9a475e76 (patch) | |
| tree | 7031e72f7f27fe22882495eeb2ae4473cc4928f8 /tactics | |
| parent | 1940c09b78fac58af7aa4c3c08913a98d5f5b04c (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/setoid_replace.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index c58400d39..cf0388543 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 _ = |