diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/quot.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tests/quot.v b/tests/quot.v index c9aa1f9d14..4fa9c4fa4e 100644 --- a/tests/quot.v +++ b/tests/quot.v @@ -7,3 +7,10 @@ Ltac2 ref1 () := reference:(nat). Ltac2 ref2 () := reference:(Datatypes.nat). Fail Ltac2 ref () := reference:(i_certainly_dont_exist). Fail Ltac2 ref () := reference:(And.Me.neither). + +Goal True. +Proof. +let x := constr:(I) in +let y := constr:((fun z => z) $x) in +Control.refine (fun _ => y). +Qed. |