From 6e025b996658458821811a46d7328a6ad8c75e2c Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 1 Nov 2005 22:37:37 +0000
Subject: Interactive test of Back

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7486 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/interactive/Back.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/interactive/Back.v

(limited to 'test-suite/interactive')

diff --git a/test-suite/interactive/Back.v b/test-suite/interactive/Back.v
new file mode 100644
index 000000000..b813a79ab
--- /dev/null
+++ b/test-suite/interactive/Back.v
@@ -0,0 +1,8 @@
+(* Check that reset remains synchronised with the compilation unit cache *)
+(* See bug #1030 *)
+
+Section multiset_defs.
+  Require Import Plus.
+End multiset_defs.
+Unset Implicit Arguments.
+Back 1.
-- 
cgit v1.2.3