diff options
| author | Matej Košík | 2018-05-07 13:11:34 +0200 |
|---|---|---|
| committer | Matej Košík | 2018-05-07 13:11:34 +0200 |
| commit | 42bd3548b84283259eae452c7bce56dfa02fb3c4 (patch) | |
| tree | 7385428784d8609827995895766af07c620ae921 | |
| parent | a7bf1793f1e570097a745060f04bc9ad8fb1d752 (diff) | |
fix some details
| -rw-r--r-- | tuto2/src/demo.ml4 | 11 |
1 files changed, 0 insertions, 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 *) |