From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 Jul 2005 09:19:06 +0000 (+0000)
Subject: The fix and cofix cases of the select were not finished. Done.
X-Git-Tag: V_0_7_1~2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=892abe32cb524599439741585f8fe502615ff23e;p=helm.git

The fix and cofix cases of the select were not finished. Done.
---

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index f390b0e42..712d8ba58 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -194,26 +194,32 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
            ) (subst,metasenv,ugraph,[]) patterns
          in
           subst,metasenv,ugraph,resoutty @ resindterm @ respatterns
-(*CSC: c'e' ancora un problema: il caso vs Meta puo' alterare il goal ==>
-       bisogna ricominciare da capo sul nuovo goal per preservare i puntatori
-       fisici
       | Cic.Fix (_, funl) -> 
          let tys =
           List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
          in
           List.fold_left (
-            fun acc (_, _, ty, bo) ->
-             find context w ty @ find (tys @ context) w bo @ acc
-          ) [] funl
+            fun (subst,metasenv,ugraph,acc) (_, _, ty, bo) ->
+             let subst,metasenv,ugraph,resty =
+              find subst metasenv ugraph context w ty in
+             let subst,metasenv,ugraph,resbo =
+              find subst metasenv ugraph (tys @ context) w bo
+             in
+              subst,metasenv,ugraph, resty @ resbo @ acc
+          ) (subst,metasenv,ugraph,[]) funl
       | Cic.CoFix (_, funl) ->
          let tys =
           List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
          in
           List.fold_left (
-            fun acc (_, ty, bo) ->
-             find context w ty @ find (tys @ context) w bo @ acc
-          ) [] funl
-*)
+            fun (subst,metasenv,ugraph,acc) (_, ty, bo) ->
+             let subst,metasenv,ugraph,resty =
+              find subst metasenv ugraph context w ty in
+             let subst,metasenv,ugraph,resbo =
+              find subst metasenv ugraph (tys @ context) w bo
+             in
+              subst,metasenv,ugraph, resty @ resbo @ acc
+          ) (subst,metasenv,ugraph,[]) funl
   in
   find subst metasenv ugraph context wanted t