From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- test-suite/ssr/intro_noop.v | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 test-suite/ssr/intro_noop.v (limited to 'test-suite/ssr/intro_noop.v') diff --git a/test-suite/ssr/intro_noop.v b/test-suite/ssr/intro_noop.v new file mode 100644 index 00000000..fdc85173 --- /dev/null +++ b/test-suite/ssr/intro_noop.v @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* bool -> bool. Proof. by []. Qed. + +Reserved Notation " a -/ b " (at level 0). +Reserved Notation " a -// b " (at level 0). +Reserved Notation " a -/= b " (at level 0). +Reserved Notation " a -//= b " (at level 0). + +Lemma test : forall a b c, a || b || c. +Proof. +move=> ---a--- - -/=- -//- -/=- -//=- b [|-]. +move: {-}a => /v/v-H; have _ := H I I. +Fail move: {-}a {H} => /v-/v-H. +have - -> : a = (id a) by []. +have --> : a = (id a) by []. +have - - _ : a = (id a) by []. +have -{1}-> : a = (id a) by []. + by myadmit. +move: a. +case: b => -[] //. +by myadmit. +Qed. -- cgit v1.2.3