Mercurial > cpdt > repo
diff src/GeneralRec.v @ 534:ed829eaa91b2
Builds with Coq 8.5beta2
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 05 Aug 2015 14:46:55 -0400 |
| parents | 8f9f1e5b2fe3 |
| children | 2c8c693ddaba |
line wrap: on
line diff
--- a/src/GeneralRec.v Tue Apr 07 18:59:24 2015 -0400 +++ b/src/GeneralRec.v Wed Aug 05 14:46:55 2015 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2006, 2011-2012, Adam Chlipala +(* Copyright (c) 2006, 2011-2012, 2015, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -8,11 +8,12 @@ *) (* begin hide *) -Require Import Arith List. +Require Import Arith List Omega. -Require Import CpdtTactics Coinductive. +Require Import Cpdt.CpdtTactics Cpdt.Coinductive. Set Implicit Arguments. +Set Asymmetric Patterns. (* end hide *)