diff options
| -rw-r--r-- | test-suite/success/forward.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v new file mode 100644 index 000000000..0ed5b524f --- /dev/null +++ b/test-suite/success/forward.v @@ -0,0 +1,18 @@ +(* 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. |