From 7741c4884d5823ed745da0c979cfb7322f0902c2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 4 Apr 2018 10:52:35 +0200
Subject: ssr: check cleared hyps do exist (fix #7050)

---
 test-suite/output/ssr_clear.out | 3 +++
 test-suite/output/ssr_clear.v   | 6 ++++++
 2 files changed, 9 insertions(+)
 create mode 100644 test-suite/output/ssr_clear.out
 create mode 100644 test-suite/output/ssr_clear.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
new file mode 100644
index 000000000..151595406
--- /dev/null
+++ b/test-suite/output/ssr_clear.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
+No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v
new file mode 100644
index 000000000..573ec47e0
--- /dev/null
+++ b/test-suite/output/ssr_clear.v
@@ -0,0 +1,6 @@
+Require Import ssreflect.
+
+Example foo : True -> True.
+Proof.
+Fail move=> {NO_SUCH_NAME}.
+Abort.
-- 
cgit v1.2.3