From 892abe32cb524599439741585f8fe502615ff23e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Jul 2005 09:19:06 +0000 Subject: [PATCH] The fix and cofix cases of the select were not finished. Done. --- helm/ocaml/tactics/proofEngineHelpers.ml | 26 +++++++++++++++--------- 1 file changed, 16 insertions(+), 10 deletions(-) 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 -- 2.39.2