diff src/DepList.v @ 534:ed829eaa91b2

Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents ad315efc3b6b
children 81d63d9c1cc5
line wrap: on
line diff
--- a/src/DepList.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/DepList.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2008-2009, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -9,9 +9,10 @@
 
 (* Dependent list types presented in Chapter 9 *)
 
-Require Import Arith List CpdtTactics.
+Require Import Arith List Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 
 Section ilist.