diff options
| author | Florent Hivert | 2016-11-17 01:33:36 +0100 |
|---|---|---|
| committer | Florent Hivert | 2016-11-17 01:33:36 +0100 |
| commit | 84cc11db01159b17a8dcf4d02dbe0549067d228f (patch) | |
| tree | 964ee247bbf305022235217e716578a37be0bf62 /mathcomp/ssrtest/first_n.v | |
| parent | 5daf14d44b9cd22c6b51b2b23b4eebe5f3aee79f (diff) | |
| parent | 23e57fb47874331c5feaace883513b7abecdff28 (diff) | |
Merge remote-tracking branch 'upstream/master' into fixdoc
Diffstat (limited to 'mathcomp/ssrtest/first_n.v')
| -rw-r--r-- | mathcomp/ssrtest/first_n.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v index 2cb6c32..126f8a5 100644 --- a/mathcomp/ssrtest/first_n.v +++ b/mathcomp/ssrtest/first_n.v @@ -1,11 +1,11 @@ -(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. 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. |