diff options
| author | Enrico Tassi | 2018-04-20 10:34:04 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:34:04 +0200 |
| commit | 09bebb67443c0512e01d2c32f4207e09e93f4956 (patch) | |
| tree | 1b88236cab5e750861008e44014ef6114b4010dc /mathcomp/ssrtest/typeof.v | |
| parent | 32496ef57916dc9fc24b53f52832ef29cf206468 (diff) | |
| parent | d54b8dff818f0b1218df14cfb2b813da93154fa9 (diff) | |
Merge remote-tracking branch 'origin/pr/189'
Diffstat (limited to 'mathcomp/ssrtest/typeof.v')
| -rw-r--r-- | mathcomp/ssrtest/typeof.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/mathcomp/ssrtest/typeof.v b/mathcomp/ssrtest/typeof.v deleted file mode 100644 index f2cb1d4..0000000 --- a/mathcomp/ssrtest/typeof.v +++ /dev/null @@ -1,12 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - -Ltac mycut x := - let tx := type of x in - cut tx. - -Lemma test : True. -Proof. -by mycut I=> [ x | ]; [ exact x | exact I ]. -Qed.
\ No newline at end of file |