From 4f64c2fd8af07a46de744af55c4a27834513f446 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 17 Jun 2017 17:57:33 +0200
Subject: 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).
---
 test-suite/bugs/closed/5434.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/5434.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5434.v b/test-suite/bugs/closed/5434.v
new file mode 100644
index 0000000000..5d2460face
--- /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.
-- 
cgit v1.2.3