support for _ in binders, and a more coplex pattern that should help if

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 3382c4c98cd0f62028080fe3b296a09a169ac317..20e8341a6c90d987a401491902a26898f85f7818 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -170,11 +170,22 @@ let select ~term ~pattern =
               (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> []))
             ctxt1 ctxt2)
     | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2
-    | Cic.Prod (_, s1, t1), Cic.Prod (name, s2, t2)
-    | Cic.Lambda (_, s1, t1), Cic.Lambda (name, s2, t2) ->
+    | Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2)
+    | Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) ->
         aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
-    | Cic.LetIn (_, s1, t1), Cic.LetIn (name, s2, t2) -> 
+    | Cic.Prod (Cic.Name n1, s1, t1), 
+      Cic.Prod ((Cic.Name n2) as name , s2, t2)
+    | Cic.Lambda (Cic.Name n1, s1, t1), 
+      Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2->
+        aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
+    | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
+    | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
+    | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> 
+        aux i s1 s2 @ aux (add_ctx i 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 i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2
+    | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
     | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2
     | Cic.Var (_, subst1), Cic.Var (_, subst2)
     | Cic.Const (_, subst1), Cic.Const (_, subst2)