diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-15 22:31:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-16 12:17:39 +0200 |
| commit | b82f27726f5ae891689e3b958323c2a61d4c154b (patch) | |
| tree | 6c0d07aa6309e5526d931031a7faf47a7ac902e9 /test-suite/success/ltac.v | |
| parent | cd3971e53b76cb62e14822eb3e275d3968a4f215 (diff) | |
Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.
Diffstat (limited to 'test-suite/success/ltac.v')
| -rw-r--r-- | test-suite/success/ltac.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index ce9099059..9ab47fede 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,9 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. + +(* Test evar syntax *) + +Goal True. +evar (0=0). +Abort. |