diff --git a/data/tutorials/platform/1_02_rocq_docs.md b/data/tutorials/platform/1_02_rocq_docs.md index c8701442..cfb4fac9 100644 --- a/data/tutorials/platform/1_02_rocq_docs.md +++ b/data/tutorials/platform/1_02_rocq_docs.md @@ -30,4 +30,6 @@ category: "Documentation" - Template Polymorphism vs. Universe Polymorphism: [interactive version](https://coq.inria.fr/platform-docs/Explanation_Template_Polymorphism.html) and [source code](https://coq.inria.fr/platform-docs/Explanation_Template_Polymorphism.v) +- Explanation of bidirectionality hints: [interactive version](https://coq.inria.fr/platform-docs/Explanation_Bidirectionality_Hints.html) + and [source code](https://coq.inria.fr/platform-docs/Explanation_Bidirectionality_Hints.v)