diff options
Diffstat (limited to 'mathcomp')
| -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. |