From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 24 Jun 2005 17:21:25 +0000 (+0000)
Subject: stupid rename
X-Git-Tag: INDEXING_NO_PROOFS~67
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e0de9924a24c8b34b3738ba343334f761c3471d;p=helm.git

stupid rename
---

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index c1f4ebc3c..61d46e24a 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -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