Implementation of locate_in finished.

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 4224eb5b154ba117ca0c2c2093adb601507afd55..a0fef6037982b57a0847d3d2ca98b8ac0636f149 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -574,40 +574,29 @@ let locate_in_term what ~where =
     | Cic.Prod (name, s, t)
     | Cic.Lambda (name, s, t) ->
         aux context s @ aux (add_ctx context name (Cic.Decl s)) t
+    | Cic.LetIn (name, s, t) -> 
+        aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
     | Cic.Appl tl -> auxs context tl
-(*
-    | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> 
-        aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
-    | Cic.LetIn (Cic.Name n1, s1, t1), 
-      Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> 
-        aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
-    | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
-    | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
-        aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2
-    | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
+    | Cic.MutCase (_, _, out, t, pat) ->
+        aux context out @ aux context t @ auxs context pat
+    | Cic.Fix (_, funs) ->
        let tys =
-        List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+        List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
        in
         List.concat
-          (List.map2
-            (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> 
-              aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
-            funs1 funs2)
-    | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
+          (List.map
+            (fun (_, _, ty, bo) -> 
+              aux context ty @ aux (tys @ context) bo)
+            funs)
+    | Cic.CoFix (_, funs) ->
        let tys =
-        List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+        List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
        in
         List.concat
-          (List.map2
-            (fun (_, ty1, bo1) (_, ty2, bo2) ->
-              aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
-            funs1 funs2)
-    | x,y -> 
-        raise (Bad_pattern 
-                (Printf.sprintf "Pattern %s versus term %s" 
-                  (CicPp.ppterm x)
-                  (CicPp.ppterm y)))
-*)
+          (List.map
+            (fun (_, ty, bo) ->
+              aux context ty @ aux (tys @ context) bo)
+            funs)
   and auxs context tl =  (* as aux for list of terms *)
     List.concat (List.map (fun t -> aux context t) tl)
   in