implemented lazy disambiguation of tactics arguments, when those

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 5c9b1f7a0ef46e7ddded1ea53911c7d5852b93b0..a7c1d39bd1953073fff0228f9556c59210047599 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -309,12 +309,10 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
             [] -> [],metasenv,ugraph,[]
           | (context',where)::tl ->
              let subst,metasenv,ugraph,tl' = find_in_roots tl in
-             let context'_len = List.length context' in
              let subst,metasenv,ugraph,found =
-              let wanted =
-               CicSubstitution.lift (context'_len - context_len) wanted
-              in
-               find_subterms ~subst ~metasenv ~ugraph ~wanted ~context where
+              let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
+               find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
+                where
              in
               subst,metasenv,ugraph,found @ tl'
         in
@@ -494,30 +492,12 @@ exception Fail of string
             | None ->
                subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
             | Some pat ->
-               try
-                let what =
-                 match what with
-                    None -> None
-                  | Some what ->
-                     let what,subst',metasenv' =
-                      CicMetaSubst.delift_rels [] metasenv
-                       (context_len - List.length context) what
-                     in
-                      assert (subst' = []);
-                      assert (metasenv' = metasenv);
-                      Some what in
                 let subst,metasenv,ugraph,terms =
                  select_in_term ~metasenv ~context ~ugraph ~term
                   ~pattern:(what,pat)
                 in
                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
-                  (entry::context)
-               with
-                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-                 raise
-                  (Fail
-                    ("The term the user wants to convert is not closed " ^
-                     "in the context of the position of the substitution.")))
+                  (entry::context))
         | Some (name,Cic.Def (bo, ty)) ->
             (match find_pattern_for name with
             | None ->
@@ -525,18 +505,6 @@ exception Fail of string
                 subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
                  (entry::context)
             | Some pat -> 
-               try
-                let what =
-                 match what with
-                    None -> None
-                  | Some what ->
-                     let what,subst',metasenv' =
-                      CicMetaSubst.delift_rels [] metasenv
-                       (context_len - List.length context) what
-                     in
-                      assert (subst' = []);
-                      assert (metasenv' = metasenv);
-                      Some what in
                 let subst,metasenv,ugraph,terms_bo =
                  select_in_term ~metasenv ~context ~ugraph ~term:bo
                   ~pattern:(what,pat) in
@@ -551,13 +519,7 @@ exception Fail of string
                       subst,metasenv,ugraph,Some res
                 in
                  subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
-                  (entry::context)
-               with
-                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-                 raise
-                  (Fail
-                    ("The term the user wants to convert is not closed " ^
-                     "in the context of the position of the substitution.")))
+                  (entry::context))
       ) context (subst,metasenv,ugraph,[],[]))
     in
      subst,metasenv,ugraph,res