From 691bb5a14ed0be69b70db0dfa0d4dcae280d2cd4 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 5 Oct 2004 18:36:28 +0000
Subject: * [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whether  
 there exists an i such that (c x1 ... xi) is a morphism. Previously   only
 the case c was tried. * [ bug fixed ]: the term that must be replaced must
 not occur in c   (i.e. in (c x1 ... xi))

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

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 6d26631254..ac0858a9de 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1122,19 +1122,39 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
     match kind_of_term in_c with
       | App (c,al) -> 
          let mors_and_cs_and_als =
-          try
-           (*CSC: we should also look the table for (c al') where
-             al' is a prefix of al *)
-           let morphisms =
-            List.map relation_morphism_of_constr_morphism
-             (morphism_table_find c) in
-           let mors_and_cs_and_als =
-            List.map (unify_morphism_with_arguments gl (c,al)) morphisms
+          let mors_and_cs_and_als =
+           let morphism_table_find c =
+            try morphism_table_find c with Not_found -> [] in
+           let rec aux acc =
+            function
+               [] ->
+                let c' = mkApp (c, Array.of_list acc) in
+                let al' = [||] in
+                List.map (fun m -> m,c',al') (morphism_table_find c')
+             | (he::tl) as l ->
+                let c' = mkApp (c, Array.of_list acc) in
+                let al' = Array.of_list l in
+                let acc' = acc @ [he] in
+                 (List.map (fun m -> m,c',al') (morphism_table_find c')) @
+                  (aux acc' tl)
            in
-            List.filter
-             (fun (mor,_,_) -> subrelation gl mor.output output_relation)
+            aux [] (Array.to_list al) in
+          let mors_and_cs_and_als =
+           List.filter (function (_,c,_) -> not (dependent t c))
+            mors_and_cs_and_als in
+          let mors_and_cs_and_als =
+           List.map
+            (function (m,c,al) ->
+              relation_morphism_of_constr_morphism m, c, al)
+             mors_and_cs_and_als in
+          let mors_and_cs_and_als =
+           List.map
+            (function (m,c,al) -> unify_morphism_with_arguments gl (c,al) m)
              mors_and_cs_and_als
-          with Not_found -> []
+          in
+           List.filter
+            (fun (mor,_,_) -> subrelation gl mor.output output_relation)
+            mors_and_cs_and_als
          in
           (* First we look for well typed morphisms *)
           let res_mors =
-- 
cgit v1.2.3