From 7fbb53b1649627b3f765fc9516becd3cd1674464 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 29 Apr 2019 20:05:58 +0200
Subject: Mini-test.

---
 test-suite/success/change.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index a9821b027f..5a8f735151 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -68,3 +68,11 @@ eassumption.
 match goal with |- ?x=1 => change (x=1) with (0+x=1) end.
 match goal with |- 0+1=1 => trivial end.
 Qed.
+
+(* Mini-check that no_check does not check *)
+
+Goal False.
+change_no_check True.
+exact I.
+Fail Qed.
+Abort.
-- 
cgit v1.2.3