diff options
| author | Pierre-Marie Pédrot | 2017-09-14 00:15:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-14 00:36:18 +0200 |
| commit | c53fb4be8c65a89dd03d4aedc2fc65d9807da915 (patch) | |
| tree | 62c830e3c4262ba306dee2dda7ef1141fd45be41 /tests | |
| parent | 4ed40a9427f67ab6091f1af5457ffdec5e156d12 (diff) | |
Binding the pose/set family of tactics.
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/example2.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index a7eb02050b..b667e19bbd 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -208,3 +208,17 @@ Proof. refine '(let x := 0 in _). eexists; exists &x; reflexivity. Qed. + +Goal True. +Proof. +pose (X := True). +constructor. +Qed. + +Goal True. +Proof. +let x := @foo in +set ($x := True) in * |-. +constructor. +Qed. + |