From 891178786f34efa1cff87e563ffa0596057f1f13 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 29 Sep 2004 13:28:08 +0000
Subject: 1. major code clean-up for the Prod case 2. cleaner behaviour:
 occurrences of the pattern in the type of a variable    bound by a dependent
 product are no longer

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

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 77a5f21162..4045816eba 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1053,26 +1053,13 @@ let mark_occur gl t in_c input_relation input_direction =
            elim_duplicates identity (res_functions @ res_mors)
       | Prod (_, c1, c2) -> 
           if (dependent (mkRel 1) c2)
-          then [ToKeep (in_c,output_relation,output_direction)]
+          then
+           errorlabstrm "Setoid_replace"
+            (str "Cannot rewrite in the type of a variable bound " ++
+             str "in a dependent product.")
           else 
-           (*CSC: output_relation in the two lines below is a bug.
-             I should use the two arguments of the relation associated to
-             coq_impl. Indeed all the Prod case is a bit hackerish. *)
-           let c1m =
-            aux output_relation (opposite_direction output_direction) c1 in
-           let c2m =
-            aux output_relation output_direction c2
-           in
-            let a = cartesian_product [| c1m ; c2m |] in
-             List.fold_left
-              (fun res a ->
-                if get_mark a
-                then
-                 (* this can be optimized since c1 and c2 will be *)
-                 (* processed again                               *)
-                 (aux output_relation output_direction
-                  (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))) @ res
-                else (ToKeep (in_c,output_relation,output_direction))::res) [] a
+           aux output_relation output_direction
+            (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))
       | _ -> [ToKeep (in_c,output_relation,output_direction)]
  in
   let aux2 output_relation output_direction =
-- 
cgit v1.2.3