summaryrefslogtreecommitdiffstats
path: root/site/posts/AlgebraicDatatypes.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-12 12:34:29 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-12 12:34:29 +0200
commit0a750a2f3cd95842f22b89bf23f92e7781291a8b (patch)
tree4e904ca3c0480db8e6f2c09649d7c0c1d73ae420 /site/posts/AlgebraicDatatypes.v
parentd5e387207fc2c21c2de1b707deacfb87770eec43 (diff)
Invert the table of contents and the revision tables
Diffstat (limited to 'site/posts/AlgebraicDatatypes.v')
-rw-r--r--site/posts/AlgebraicDatatypes.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.v
index 74bdf04..a0a83a2 100644
--- a/site/posts/AlgebraicDatatypes.v
+++ b/site/posts/AlgebraicDatatypes.v
@@ -93,9 +93,9 @@ Inductive prod (A B : Type) : Type :=
| pair : A -> B -> prod A B
>>
- #<div id="history">site/posts/AlgebraicDatatypes.v</div>#
+ #<div id="generate-toc"></div>#
- #<div id="generate-toc"></div># *)
+ #<div id="history">site/posts/AlgebraicDatatypes.v</div># *)
From Coq Require Import
Basics Setoid Equivalence Morphisms