From 42bd3548b84283259eae452c7bce56dfa02fb3c4 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 7 May 2018 13:11:34 +0200
Subject: fix some details

---
 tuto2/src/demo.ml4 | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
index 082e5cfa97..3d165a6302 100644
--- a/tuto2/src/demo.ml4
+++ b/tuto2/src/demo.ml4
@@ -1,14 +1,3 @@
-(* This will be compilable once the following pull-requests:
-   - https://github.com/coq/coq/pull/759
-   - https://github.com/coq/coq/pull/761
-   will be merged.
-
-   TODO: update the part related to "Cmd6" once I get an answer to this question:
-         https://sympa.inria.fr/sympa/arc/coqdev/2017-06/msg00037.html
-
-   TODO: figure out why does Summary.Local.ref function requires argument "name" ?
-*)   
-
 (* -------------------------------------------------------------------------- *)
 (*                                                                            *)
 (*                            Initial ritual dance                            *)
-- 
cgit v1.2.3