diff options
| author | Pierre-Marie Pédrot | 2017-08-29 01:16:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-29 01:23:32 +0200 |
| commit | db03c10aaafd3c0128a5b7504f14d4b7aaca842e (patch) | |
| tree | 47ee736fc51f6e309cad5aa26158eafcf83f06e0 /tests | |
| parent | ece1cc059c26351d05a0ef41131c663c37cb7761 (diff) | |
Implementing Ltac2 antiquotations in constr syntax.
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. |