From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/success/forward.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 test-suite/success/forward.v (limited to 'test-suite/success/forward.v') diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v new file mode 100644 index 00000000..4e36dec1 --- /dev/null +++ b/test-suite/success/forward.v @@ -0,0 +1,29 @@ +(* Testing forward reasoning *) + +Goal 0=0. +Fail assert (_ = _). +eassert (_ = _)by reflexivity. +eassumption. +Qed. + +Goal 0=0. +Fail set (S ?[nl]). +eset (S ?[n]). +remember (S ?n) as x. +instantiate (n:=0). +Fail remember (S (S _)). +eremember (S (S ?[x])). +instantiate (x:=0). +reflexivity. +Qed. + +(* Don't know if it is good or not but the compatibility tells that + the asserted goal to prove is subject to beta-iota but not the + asserted hypothesis *) + +Goal True. +assert ((fun x => x) False). +Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) +2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) +Abort. + -- cgit v1.2.3