Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").

4 files changed, 140 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v
new file mode 100644
index 000000000..2522a274f
--- /dev/null
+++ b/test-suite/bugs/closed/5414.v
@@ -0,0 +1,12 @@
+(* Use of idents bound to ltac names in a "match" *)
+
+Definition foo : Type.
+Proof.
+  let x := fresh "a" in
+  refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)).
+  exact (a = a).
+Defined.
+Goal foo.
+intros k. elim k. (* elim because elim keeps names *)
+intros.
+Check a. (* We check that the name is "a" *)
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f064dfe76..97fa8e254 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -80,3 +80,49 @@ fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
 The constructor D (in type J) expects 3 arguments.
+lem1 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+lem2 = 
+fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
+     : forall k : bool, k = k
+
+Argument scope is [bool_scope]
+lem3 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+1 subgoal
+  
+  x : nat
+  n, n0 := match x + 0 with
+           | 0 => 0
+           | S _ => 0
+           end : nat
+  e,
+  e0 := match x + 0 as y return (y = y) with
+        | 0 => eq_refl
+        | S n => eq_refl
+        end : x + 0 = x + 0
+  n1, n2 := match x with
+            | 0 => 0
+            | S _ => 0
+            end : nat
+  e1, e2 := match x return (x = x) with
+            | 0 => eq_refl
+            | S n => eq_refl
+            end : x = x
+  ============================
+  x + 0 = 0
+1 subgoal
+  
+  p : nat
+  a,
+  a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : eq_refl = eq_refl /\ p = p
+  a1,
+  a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : p = p /\ p = p
+  ============================
+  eq_refl = eq_refl
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 6a4fd007d..17fee3303 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -121,3 +121,66 @@ Check fun x => let '(D n m p q) := x in n+m+p+q.
 (* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
 
 Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
+
+(* Test use of idents bound to ltac names in a "match" *)
+
+Lemma lem1 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end).
+Qed.
+Print lem1.
+
+Lemma lem2 : forall k, k=k :> bool.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k => if k as x return x = x then eq_refl else eq_refl).
+Qed.
+Print lem2.
+
+Lemma lem3 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl).
+Qed.
+Print lem3.
+
+Lemma lem4 x : x+0=0.
+match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+Show.
+
+Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
+let y := fresh "n" in (* Checking that y is hidden *)
+  let z := fresh "e" in (* Checking that z is hidden *)
+  match goal with
+  |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let p := fresh "p" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+Show.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index e59828def..ce98879a5 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -17,3 +17,22 @@ Fail exists (fun x =>
         with
         | eq_refl => eq_refl
         end).
+Abort.
+
+(* Some tests with ltac matching on building "if" and "let" *)
+
+Goal forall b c d, (if negb b then c else d) = 0.
+intros.
+match goal with
+|- (if ?b then ?c else ?d) = 0 => transitivity (if b then d else c)
+end.
+Abort.
+
+Definition swap {A} {B} '((x,y):A*B) := (y,x).
+
+Goal forall p, (let '(x,y) := swap p in x + y) = 0.
+intros.
+match goal with
+|- (let '(x,y) := ?p in x + y) = 0 => transitivity (let (x,y) := p in x+y)
+end.
+Abort.