diff options
Diffstat (limited to 'tests/example2.v')
| -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. + |