Mercurial > cpdt > repo
comparison src/Extensional.v @ 297:b441010125d4
Everything compiles in Coq 8.3pl1
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 14 Jan 2011 14:39:12 -0500 |
parents | 2c88fc1dbe33 |
children | 7b38729be069 |
comparison
equal
deleted
inserted
replaced
296:559ec7328410 | 297:b441010125d4 |
---|---|
1 (* Copyright (c) 2008-2010, Adam Chlipala | 1 (* Copyright (c) 2008-2011, 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 String List. | 11 Require Import String List. |
12 | 12 |
13 Require Import Axioms Tactics DepList. | 13 Require Import Tactics DepList. |
14 | 14 |
15 Set Implicit Arguments. | 15 Set Implicit Arguments. |
16 (* end hide *) | 16 (* end hide *) |
17 | 17 |
18 | 18 |