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

patterns will be used on subterms.
match pattern, term with
| Binder Anonymous, Binder name -> recursion
| Binder name1, Binder name2 when name1 = name2 -> recursion
| Binder name1, Binder name2 -> []

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9443a35d14231026a95cdbf611b65f95d7a73bd0..1b67821c1ec8630a3d24dd71c7ae4c3e3e2042da 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -229,10 +229,12 @@ EXTEND
     ]];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   binder_vars: [
-      [ vars = LIST1 IDENT SEP SYMBOL ",";
+      [ vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]];
         typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-      | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
-        typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
+      | PAREN "("; 
+          vars = [ l =  LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]];
+          typ = OPT [ SYMBOL ":"; t = term -> t ]; 
+        PAREN ")" -> (vars, typ)
       ]
   ];
   term0: [ [ t = term; EOI -> return_term loc t ] ];

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)