comparison 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
comparison
equal deleted inserted replaced
226:9d0b9577f8b1 227:d8c54a25c81f
199 \hline 199 \hline
200 Reasoning About Equality Proofs & \texttt{Equality.v} \\ 200 Reasoning About Equality Proofs & \texttt{Equality.v} \\
201 \hline 201 \hline
202 Generic Programming & \texttt{Generic.v} \\ 202 Generic Programming & \texttt{Generic.v} \\
203 \hline 203 \hline
204 Universes and Axioms & \texttt{Universes.v} \\
205 \hline
204 Proof Search in Ltac & \texttt{Match.v} \\ 206 Proof Search in Ltac & \texttt{Match.v} \\
205 \hline 207 \hline
206 Proof by Reflection & \texttt{Reflection.v} \\ 208 Proof by Reflection & \texttt{Reflection.v} \\
207 \hline 209 \hline
208 First-Order Abstract Syntax & \texttt{Firstorder.v} \\ 210 First-Order Abstract Syntax & \texttt{Firstorder.v} \\