Mercurial > cpdt > repo
comparison src/Subset.v @ 534:ed829eaa91b2
Builds with Coq 8.5beta2
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 05 Aug 2015 14:46:55 -0400 |
parents | 8921cfa2f503 |
children | af97676583f3 |
comparison
equal
deleted
inserted
replaced
533:8921cfa2f503 | 534:ed829eaa91b2 |
---|---|
1 (* Copyright (c) 2008-2012, Adam Chlipala | 1 (* Copyright (c) 2008-2012, 2015, Adam Chlipala |
2 * | 2 * |
3 * This work is licensed under a | 3 * This work is licensed under a |
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
5 * Unported License. | 5 * Unported License. |
6 * The license text is available at: | 6 * The license text is available at: |
8 *) | 8 *) |
9 | 9 |
10 (* begin hide *) | 10 (* begin hide *) |
11 Require Import List. | 11 Require Import List. |
12 | 12 |
13 Require Import CpdtTactics. | 13 Require Import Cpdt.CpdtTactics. |
14 | 14 |
15 Set Implicit Arguments. | 15 Set Implicit Arguments. |
16 Set Asymmetric Patterns. | |
16 (* end hide *) | 17 (* end hide *) |
17 | 18 |
18 (** printing <-- $\longleftarrow$ *) | 19 (** printing <-- $\longleftarrow$ *) |
19 | 20 |
20 | 21 |