Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).

Ltac pattern-matching was requiring dependent variables to be named.
This "natural" expectation is however not guaranteed by unification:
an evar can be dependent on an anonymous variable, resulting in
elaborated terms with dependent anonymous variables (see example in
file 5434.v).

This commit "fixes" the problem by not requiring that dependent
variables are named in ltac pattern-matching. Ltac pattern-matching
names itself these anonymous dependent variables, using the same
strategy as the printer (i.e. using "H" to display such
internally-anonymous dependent variables).

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5434.v b/test-suite/bugs/closed/5434.v
new file mode 100644
index 000000000..5d2460fac
--- /dev/null
+++ b/test-suite/bugs/closed/5434.v
@@ -0,0 +1,18 @@
+(* About binders which remain unnamed after typing *)
+
+Global Set Asymmetric Patterns.
+
+Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x :
+@sig A P) : @sig A Q
+  := let 'exist a p := x in exist Q a (f a p).
+Axioms (feBW' : Type) (g : Prop -> Prop) (f' : feBW' -> Prop).
+Definition foo := @proj2_sig_map feBW' (fun  H  => True = f' _) (fun H =>
+ g True = g (f' H))
+                                 (fun (a : feBW') (p : (fun H : feBW' => True =
+ f' H) a) => @f_equal Prop Prop g True (f' a) p).
+Print foo.
+Goal True.
+  lazymatch type of foo with
+  | sig (fun a : ?A => ?P) -> _
+    => pose (fun a : A => a = a /\ P = P)
+  end.