8 files changed, 119 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_10812.v b/test-suite/bugs/closed/bug_10812.v
new file mode 100644
index 0000000000..68f3814781
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10812.v
@@ -0,0 +1,28 @@
+(* subst with indirectly dependent section variables *)
+
+Section A.
+
+Variable a:nat.
+Definition b := a.
+
+Goal a=1 -> a+a=1 -> b=1.
+intros.
+Fail subst a. (* was working; we make it failing *)
+rewrite H in H0.
+discriminate.
+Qed.
+
+Goal a=1 -> a+a=1 -> b=1.
+intros.
+subst. (* should not apply to a *)
+rewrite H in H0.
+discriminate.
+Qed.
+
+Goal forall t, a=t -> b=t.
+intros.
+subst.
+reflexivity.
+Qed.
+
+End A.
diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index e1c20a2059..7b3a460c8c 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -15,6 +15,39 @@ Fail foo ().
 constructor.
 Qed.
 
+
+(** Bindings are dynamic *)
+
+Ltac2 Type rec nat := [O | S (nat)].
+
+Ltac2 rec nat_eq n m :=
+  match n with
+  | O => match m with | O => true | S _ => false end
+  | S n => match m with | O => false | S m => nat_eq n m end
+  end.
+
+Ltac2 Type exn ::= [ Assertion_failed ].
+
+Ltac2 assert_eq n m :=
+  match nat_eq n m with
+  | true => ()
+  | false => Control.throw Assertion_failed end.
+
+Ltac2 mutable x := O.
+Ltac2 y := x.
+Ltac2 Eval (assert_eq y O).
+Ltac2 Set x := (S O).
+Ltac2 Eval (assert_eq y (S O)).
+
+Ltac2 mutable quw := fun (n : nat) => O.
+Ltac2 Set quw := fun n =>
+  match n with
+  | O => O
+  | S n => S (S (quw n))
+  end.
+
+Ltac2 Eval (quw (S (S O))).
+
 (** Not the right type *)
 Fail Ltac2 Set foo := 0.
 
@@ -25,10 +58,46 @@ Fail Ltac2 Set bar := fun _ => ().
 
 (** Subtype check *)
 
-Ltac2 mutable rec f x := f x.
+Ltac2 rec h x := h x.
 
+Ltac2 mutable f x := h x.
 Fail Ltac2 Set f := fun x => x.
 
 Ltac2 mutable g x := x.
+Ltac2 Set g := h.
+
+(** Rebinding with old values *)
+
+
+
+Ltac2 mutable qux n := S n.
+
+Ltac2 Set qux as self := fun n => self (self n).
+
+Ltac2 Eval assert_eq (qux O) (S (S O)).
+
+Ltac2 mutable quz := O.
+
+Ltac2 Set quz as self := S self.
+
+Ltac2 Eval (assert_eq quz (S O)).
+
+Ltac2 rec addn n :=
+  match n with
+  | O => fun m => m
+  | S n => fun m => S (addn n m)
+
+  end.
+Ltac2 mutable rec quy n :=
+  match n with
+  | O => S O
+  | S n => S (quy n)
+  end.
 
-Ltac2 Set g := f.
+Ltac2 Set quy as self := fun n =>
+                           match n with
+                           | O => O
+                           | S n => addn (self n) (quy n)
+                           end.
+Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))).
+Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))).
diff --git a/test-suite/output/ErrorLocation_12152_1.out b/test-suite/output/ErrorLocation_12152_1.out
new file mode 100644
index 0000000000..b7b600d53d
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12152_1.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 0-7:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v
new file mode 100644
index 0000000000..e63ab1cd48
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12152_1.v
@@ -0,0 +1,3 @@
+(* Reported in #12152 *)
+Goal True.
+intro H; auto.
diff --git a/test-suite/output/ErrorLocation_12152_2.out b/test-suite/output/ErrorLocation_12152_2.out
new file mode 100644
index 0000000000..bdfd0a050f
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12152_2.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 0-8:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v
new file mode 100644
index 0000000000..5df6bec939
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12152_2.v
@@ -0,0 +1,3 @@
+(* Reported in #12152 *)
+Goal True.
+intros H; auto.
diff --git a/test-suite/output/ErrorLocation_12255.out b/test-suite/output/ErrorLocation_12255.out
new file mode 100644
index 0000000000..ed5e183427
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12255.out
@@ -0,0 +1,4 @@
+File "stdin", line 4, characters 0-16:
+Error: Ltac variable x is bound to i > 0 which cannot be coerced to
+an evaluable reference.
+
diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v
new file mode 100644
index 0000000000..347424b2fc
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12255.v
@@ -0,0 +1,4 @@
+Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac.
+Definition i := O.
+Goal False.
+can_unfold (i>0).