From a7bf1793f1e570097a745060f04bc9ad8fb1d752 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 7 May 2018 11:09:48 +0200
Subject: fix some details

---
 tuto2/_CoqProject  | 2 +-
 tuto2/src/demo.ml4 | 6 +-----
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject
index ca139558ed..f38ee8d6a6 100644
--- a/tuto2/_CoqProject
+++ b/tuto2/_CoqProject
@@ -3,4 +3,4 @@
 
 theories/Test.v
 src/demo.ml4
-src/tuto_plugin.mlpack
\ No newline at end of file
+src/tuto_plugin.mlpack
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
index cf6a367867..082e5cfa97 100644
--- a/tuto2/src/demo.ml4
+++ b/tuto2/src/demo.ml4
@@ -6,11 +6,7 @@
    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 requre argument "name" ?
-         (Can it be any string?
-          Must it be a unique string (per each state variable?)
-          Must it be a unique string global (for all plugins)?)
-          What would happen if it were an empty string?
+   TODO: figure out why does Summary.Local.ref function requires argument "name" ?
 *)   
 
 (* -------------------------------------------------------------------------- *)
-- 
cgit v1.2.3