1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2837.v b/test-suite/bugs/closed/shouldsucceed/2837.v
new file mode 100644
index 00000000..5d984463
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2837.v
@@ -0,0 +1,15 @@
+Require Import JMeq.
+
+Axiom test : forall n m : nat, JMeq n m.
+
+Goal forall n m : nat, JMeq n m.
+
+(* I) with no intros nor variable hints, this should produce a regular error
+      instead of Uncaught exception Failure("nth"). *)
+Fail rewrite test.
+
+(* II) with intros but indication of variables, still an error *)
+Fail (intros; rewrite test).
+
+(* III) a working variant: *)
+intros; rewrite (test n m).
+\ No newline at end of file