Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Extensional.v Thu Dec 09 14:39:49 2010 -0500 +++ b/src/Extensional.v Fri Jan 14 14:39:12 2011 -0500 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2011, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -10,7 +10,7 @@ (* begin hide *) Require Import String List. -Require Import Axioms Tactics DepList. +Require Import Tactics DepList. Set Implicit Arguments. (* end hide *)