From 8e78a6dc20858ce2ca989da903e6311ffe727695 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 25 Aug 2020 14:52:16 +0200
Subject: [test-suite] close the proof

---
 test-suite/output/ssr_error_multiple_intro_after_case.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v
index 1f87966693..18997b8686 100644
--- a/test-suite/output/ssr_error_multiple_intro_after_case.v
+++ b/test-suite/output/ssr_error_multiple_intro_after_case.v
@@ -1,3 +1,4 @@
 Require Import ssreflect.
 Goal forall p : nat * nat , True.
 case => x x.
+Abort.
-- 
cgit v1.2.3