X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=cf7df2d58a197ca9895837e784aa0a94e4b47294;hb=6bbeb650abc3a94e76d683aa47b2e46254d495d1;hp=fd336910ea4a899e3d5fcdc15870bffd929afb12;hpb=99171b0e4bd02486bd99208bbca911eba03c7af7;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index fd336910e..cf7df2d58 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 exception Bad_pattern of string Lazy.t
 
 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
@@ -226,9 +228,7 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
   find subst metasenv ugraph context wanted t
   
 let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
-  let add_ctx context name entry =
-      (Some (name, entry)) :: context
-  in
+  let add_ctx context name entry = (Some (name, entry)) :: context in
   let map2 error_msg f l1 l2 = 
     try 
       List.map2 f l1 l2 
@@ -301,8 +301,11 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
     List.concat (map2 "wrong number of arguments in application"
       (fun t1 t2 -> aux context t1 t2) terms1 terms2)
   in
-   let context_len = List.length context in
-   let roots = aux context where term in
+   let roots =
+     match where with
+     | None -> []
+     | Some where -> aux context where term
+   in
     match wanted with
        None -> [],metasenv,ugraph,roots
      | Some wanted ->
@@ -474,15 +477,15 @@ exception Fail of string Lazy.t
   * @raise Bad_pattern
   * *)
   let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
-       ~pattern:(what,hyp_patterns,goal_pattern)
+       ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
   =
+   let what, hyp_patterns, goal_pattern = pattern in
    let find_pattern_for name =
      try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
      with Not_found -> None in
    let subst,metasenv,ugraph,ty_terms =
     select_in_term ~metasenv ~context ~ugraph ~term:ty
      ~pattern:(what,goal_pattern) in
-   let context_len = List.length context in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right
@@ -496,7 +499,7 @@ exception Fail of string Lazy.t
             | Some pat ->
                 let subst,metasenv,ugraph,terms =
                  select_in_term ~metasenv ~context ~ugraph ~term
-                  ~pattern:(what,pat)
+                  ~pattern:(what, Some pat)
                 in
                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
                   (entry::context))
@@ -509,14 +512,14 @@ exception Fail of string Lazy.t
             | Some pat -> 
                 let subst,metasenv,ugraph,terms_bo =
                  select_in_term ~metasenv ~context ~ugraph ~term:bo
-                  ~pattern:(what,pat) in
+                  ~pattern:(what, Some pat) in
                 let subst,metasenv,ugraph,terms_ty =
                  match ty with
                     None -> subst,metasenv,ugraph,None
                   | Some ty ->
                      let subst,metasenv,ugraph,res =
                       select_in_term ~metasenv ~context ~ugraph ~term:ty
-                       ~pattern:(what,pat)
+                       ~pattern:(what, Some pat)
                      in
                       subst,metasenv,ugraph,Some res
                 in