diff src/Intro.v @ 227:d8c54a25c81f

Update DataStruct with a new reason to use reflexive types; start Universes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 18 Nov 2009 15:38:01 -0500
parents dbac52f5bce1
children 52b9e43be069
line wrap: on
line diff
--- a/src/Intro.v	Mon Nov 16 13:27:34 2009 -0500
+++ b/src/Intro.v	Wed Nov 18 15:38:01 2009 -0500
@@ -201,6 +201,8 @@
 \hline
 Generic Programming & \texttt{Generic.v} \\
 \hline
+Universes and Axioms & \texttt{Universes.v} \\
+\hline
 Proof Search in Ltac & \texttt{Match.v} \\
 \hline
 Proof by Reflection & \texttt{Reflection.v} \\