diff options
| author | Enrico Tassi | 2016-06-17 16:38:57 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-17 16:38:57 +0200 |
| commit | 8a701c74a1fd3d05fefe48e6129c59793c5d611c (patch) | |
| tree | 0914d510d583e1afad36ce275e54a00e11d39f7b | |
| parent | e33a23bbaefea57b486f7ea136ef4d058dbb34e1 (diff) | |
fix parsing (coq trunk goal selector/ltac:)
| -rw-r--r-- | mathcomp/ssrtest/first_n.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v index 2cb6c32..3d99a0f 100644 --- a/mathcomp/ssrtest/first_n.v +++ b/mathcomp/ssrtest/first_n.v @@ -5,7 +5,7 @@ From mathcomp Require Import ssrbool. Lemma test : False -> (bool -> False -> True -> True) -> True. -move=> F; let w := 2 in apply; last w first. +move=> F; let w := constr:(2) in apply; last w first. - by apply: F. - by apply: I. by apply: true. |