]> matita.cs.unibo.it Git - helm.git/commitdiff
stupid rename
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 24 Jun 2005 17:21:25 +0000 (17:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 24 Jun 2005 17:21:25 +0000 (17:21 +0000)
helm/ocaml/tactics/proofEngineHelpers.ml

index c1f4ebc3c7ac58466066cbf25e7001802226b756..61d46e24aa89767e07e1a40afc96548792d235c0 100644 (file)
@@ -110,8 +110,8 @@ let compare_metasenvs ~oldmetasenv ~newmetasenv =
 
 (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
 let find_subterms ~eq ~wanted t =
-  let rec find wanted t =
-    if eq wanted t then 
+  let rec find w t =
+    if eq w t then 
       [t]
     else
       match t with
@@ -122,31 +122,31 @@ let find_subterms ~eq ~wanted t =
             fun acc e -> 
               match e with 
               | None -> acc 
-              | Some t -> find wanted t @ acc
+              | Some t -> find w t @ acc
           ) [] ctx
       | Cic.Lambda (_, t1, t2) 
       | Cic.Prod (_, t1, t2) 
       | Cic.LetIn (_, t1, t2) -> 
-          find wanted t1 @ find (CicSubstitution.lift 1 wanted) t2
+          find w t1 @ find (CicSubstitution.lift 1 w) t2
       | Cic.Appl l -> 
-          List.fold_left (fun acc t -> find wanted t @ acc) [] l
-      | Cic.Cast (t, ty) -> find wanted t @ find wanted ty
+          List.fold_left (fun acc t -> find w t @ acc) [] l
+      | Cic.Cast (t, ty) -> find w t @ find w ty
       | Cic.Implicit _ -> assert false
       | Cic.Const (_, esubst)
       | Cic.Var (_, esubst) 
       | Cic.MutInd (_, _, esubst) 
       | Cic.MutConstruct (_, _, _, esubst) -> 
-          List.fold_left (fun acc (_, t) -> find wanted t @ acc) [] esubst
+          List.fold_left (fun acc (_, t) -> find w t @ acc) [] esubst
       | Cic.MutCase (_, _, outty, indterm, patterns) -> 
-          find wanted outty @ find wanted indterm @ 
-            List.fold_left (fun acc p -> find wanted p @ acc) [] patterns
+          find w outty @ find w indterm @ 
+            List.fold_left (fun acc p -> find w p @ acc) [] patterns
       | Cic.Fix (_, funl) -> 
           List.fold_left (
-            fun acc (_, _, ty, bo) -> find wanted ty @ find wanted bo @ acc
+            fun acc (_, _, ty, bo) -> find w ty @ find w bo @ acc
           ) [] funl
       | Cic.CoFix (_, funl) ->
           List.fold_left (
-            fun acc (_, ty, bo) -> find wanted ty @ find wanted bo @ acc
+            fun acc (_, ty, bo) -> find w ty @ find w bo @ acc
           ) [] funl
   in
   find wanted t