# HG changeset patch # User Adam Chlipala # Date 1443804854 14400 # Node ID af5de2d0b4edf714c0be321358236b14b45f21cc # Parent f874c163f5e002c1194473569d7f2523d0de0660 Fix HTML filename convention diff -r f874c163f5e0 -r af5de2d0b4ed src/toc.html --- a/src/toc.html Fri Oct 02 12:49:58 2015 -0400 +++ b/src/toc.html Fri Oct 02 12:54:14 2015 -0400 @@ -4,23 +4,23 @@

Certified Programming with Dependent Types

-
  • Introduction -
  • Some Quick Examples -
  • Introducing Inductive Types -
  • Inductive Predicates -
  • Infinite Data and Proofs -
  • Subset Types and Variations -
  • General Recursion -
  • More Dependent Types -
  • Dependent Data Structures -
  • Reasoning About Equality Proofs -
  • Generic Programming -
  • Universes and Axioms -
  • Proof Search by Logic Programming -
  • Proof Search in Ltac -
  • Proof by Reflection -
  • Proving in the Large -
  • A Taste of Reasoning About Programming Language Syntax -
  • Conclusion +
  • Introduction +
  • Some Quick Examples +
  • Introducing Inductive Types +
  • Inductive Predicates +
  • Infinite Data and Proofs +
  • Subset Types and Variations +
  • General Recursion +
  • More Dependent Types +
  • Dependent Data Structures +
  • Reasoning About Equality Proofs +
  • Generic Programming +
  • Universes and Axioms +
  • Proof Search by Logic Programming +
  • Proof Search in Ltac +
  • Proof by Reflection +
  • Proving in the Large +
  • A Taste of Reasoning About Programming Language Syntax +
  • Conclusion