2 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12011.v b/test-suite/bugs/closed/bug_12011.v
new file mode 100644
index 0000000000..f149b4e8ae
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12011.v
@@ -0,0 +1,21 @@
+From Coq Require Import Setoid ssreflect.
+
+Lemma test A (R : relation A) `{Equivalence _ R} (x y z : A) :
+  R x y -> R y z -> R x z.
+Proof.
+  intros Hxy Hyz.
+  rewrite -Hxy in Hyz.
+  exact Hyz.
+Qed.
+
+
+
+Axiom envs_lookup_delete : bool.
+Axiom envs_lookup_delete_Some : envs_lookup_delete = true <-> False.
+
+Goal envs_lookup_delete = true -> False.
+Proof.
+intros Hlookup.
+rewrite envs_lookup_delete_Some in Hlookup *. (* <- used to revert Hlookup *)
+exact Hlookup.
+Qed.
diff --git a/test-suite/ltac2/printf.v b/test-suite/ltac2/printf.v
new file mode 100644
index 0000000000..f96a01a9c9
--- /dev/null
+++ b/test-suite/ltac2/printf.v
@@ -0,0 +1,31 @@
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Printf.
+
+(* Check that the arguments have type unit *)
+Ltac2 ignore (x : unit) := ().
+
+Ltac2 dummy (_ : unit) (_ : int) := Message.of_string "dummy".
+
+(** Simple test for all specifications *)
+
+Ltac2 Eval ignore (printf "%i" 42).
+Ltac2 Eval ignore (printf "%s" "abc").
+Ltac2 Eval ignore (printf "%I" @Foo).
+Ltac2 Eval ignore (printf "%t" '(1 + 1 = 0)).
+Ltac2 Eval ignore (printf "%%").
+Ltac2 Eval ignore (printf "%a" dummy 18).
+
+(** More complex tests *)
+
+Ltac2 Eval ignore (printf "%I foo%a bar %s" @ok dummy 18 "yes").
+
+Ltac2 Eval Message.print (fprintf "%I foo%a bar %s" @ok dummy 18 "yes").
+
+(** Failure tests *)
+
+Fail Ltac2 Eval printf "%i" "foo".
+Fail Ltac2 Eval printf "%s" 0.
+Fail Ltac2 Eval printf "%I" "foo".
+Fail Ltac2 Eval printf "%t" "foo".
+Fail Ltac2 Eval printf "%a" (fun _ _ => ()).
+Fail Ltac2 Eval printf "%a" (fun _ i => Message.of_int i) "foo".