Import DeBruijn

Makefile

@@ -2,7 +2,7 @@ MODULES_NODOC := Axioms Tactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality Generic Universes Match Reflection \
-	Large Firstorder Hoas Interps Extensional Intensional OpSem
+	Large Firstorder DeBruijn Hoas Interps Extensional Intensional OpSem
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)

src/Intro.v

@@ -215,6 +215,8 @@ Proving in the Large & \texttt{Large.v} \\
 \hline
 First-Order Abstract Syntax & \texttt{Firstorder.v} \\
 \hline
+Dependent De Bruijn Indices & \texttt{DeBruijn.v} \\
+\hline
 Higher-Order Abstract Syntax & \texttt{Hoas.v} \\
 \hline
 Type-Theoretic Interpreters & \texttt{Interps.v} \\

src/OpSem.v

-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2009, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0

src/toc.html

@@ -19,6 +19,7 @@
 <li><a href="Reflection.html">Proof by Reflection</a>
 <li><a href="Large.html">Proving in the Large</a>
 <li><a href="Firstorder.html">First-Order Abstract Syntax</a>
+<li><a href="DeBruijn.html">Dependent De Bruijn Indices</a>
 <li><a href="Hoas.html">Higher-Order Abstract Syntax</a>
 <li><a href="Interps.html">Type-Theoretic Interpreters</a>
 <li><a href="Extensional.html">Extensional Transformations</a>