8 files changed, 97 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v
new file mode 100644
index 0000000000..2cf91c1c2b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9114.v
@@ -0,0 +1,5 @@
+Goal True.
+  assert_succeeds (exact I).
+  idtac.
+  (* Error: No such goal. *)
+Abort.
diff --git a/test-suite/ltac2/ltac2env.v b/test-suite/ltac2/ltac2env.v
new file mode 100644
index 0000000000..743e62932d
--- /dev/null
+++ b/test-suite/ltac2/ltac2env.v
@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
+
+Goal True.
+Proof.
+(* Fails at runtime because not fully applied *)
+Fail ltac1:(ltac2:(x |- ())).
+(* Type mismatch: Ltac1.t vs. constr *)
+Fail ltac1:(ltac2:(x |- pose $x)).
+(* Check that runtime cast is OK *)
+ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t nat).
+(* Type mismatch *)
+Fail ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t ident:(foo)).
+Abort.
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out
new file mode 100644
index 0000000000..285a3bcd89
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.out
@@ -0,0 +1,42 @@
+
+Coq < Coq < 1 subgoal
+  
+  ============================
+  [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x < 
+x < 1 focused subgoal
+(shelved: 1)
+  [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+  ============================
+  [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused subgoal
+(shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused subgoals
+(shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[0m
+
+subgoal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m?j[49m
+   [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+      [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x < 
diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v
new file mode 100644
index 0000000000..4251c52cb4
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.v
@@ -0,0 +1,6 @@
+(* coq-prog-args: ("-color" "on" "-diffs" "on") *)
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.  Show Proof Diffs.
+  eexists.  Show Proof Diffs.
+  split.  Show Proof Diffs.
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 19c9fc4423..70427220ed 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -6,3 +6,4 @@ The command has indeed failed with message:
 H is already used.
 The command has indeed failed with message:
 H is already used.
+a
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index fa12f09a46..96b6d652c9 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -22,3 +22,11 @@ intros H.
 Fail intros [H%myid ?].
 Fail destruct 1 as [H%myid ?].
 Abort.
+
+
+(* Test that assert_succeeds only runs a tactic once *)
+Ltac should_not_loop := idtac + should_not_loop.
+Goal True.
+  assert_succeeds should_not_loop.
+  assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
+Abort.
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 81c9763ccd..6c333121da 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -96,10 +96,25 @@ Section visibility.
 
   Let Fixpoint by_proof (n:nat) : True.
   Proof. exact I. Defined.
+
+  Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool.
+  Proof.
+    - destruct n as [|n].
+      + exact true.
+      + exact (bar n).
+    - destruct n as [|n].
+      + exact false.
+      + exact (foo n).
+  Qed.
+
+  Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool.
+  Admitted.
+
 End visibility.
 
 Fail Check imm.
 Fail Check by_proof.
+Check bla. Check bli.
 
 Module Import mod_local.
   Fixpoint imm_importable (n:nat) : True := I.
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 381fbabe72..998f3f7dd1 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -419,13 +419,13 @@ Qed.
 
 
 
-Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point,
+Lemma Desargues: forall A B C A1 B1 C1 P Q T S:point,
   X S = 0 -> Y S = 0 -> Y A = 0 ->
   collinear A S A1 -> collinear B S B1 -> collinear C S C1 ->
   collinear B1 C1 P -> collinear B C P ->
   collinear A1 C1 Q -> collinear A C Q -> 
-  collinear A1 B1 R -> collinear A B R ->
-  collinear P Q R
+  collinear A1 B1 T -> collinear A B T ->
+  collinear P Q T
   \/ X A = X B \/ X A = X C \/ X B = X C  \/ X A = 0 \/ Y B = 0 \/ Y C = 0
   \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1.
 Proof.
@@ -440,8 +440,8 @@ let lv := rev (X A
              :: Y A1 :: X A1
                 :: Y B1
                    :: Y C1
-                      :: X R
-                         :: Y R
+                      :: X T
+                         :: Y T
                             :: X Q
                                :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in
 nsatz with radicalmax :=1%N strategy:=0%Z