Mercurial > cpdt > repo

comparison src/Coinductive.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents f02b698aadb1
children 81d63d9c1cc5
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 Definition bad : unit := tt. 15 Definition bad : unit := tt.
16 16
17 Set Implicit Arguments. 17 Set Implicit Arguments.
18 Set Asymmetric Patterns.
18 (* end hide *) 19 (* end hide *)
19 20
20 21
21 (** %\chapter{Infinite Data and Proofs}% *) 22 (** %\chapter{Infinite Data and Proofs}% *)
22 23