Commit 61f0302d authored by Andrei Paskevich's avatar Andrei Paskevich

update ROADMAP

parent 3070b01d
......@@ -65,15 +65,8 @@
* doc: citer l'article Boogie 2011 quelque part
* Check if remark in doc/api.tex line 80 is still valid (A)
* increment the magic number in config (A)
* deplacer le bouton "Cancel" dans le menu "tools",
le renommer en "make obsolete" et le documenter (A)
* document new Why options (A)
* Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs
(JC)
......@@ -85,6 +78,13 @@
* document new IDE features (C)
* document "Make obsolete" (A)
* DONE deplacer le bouton "Cancel" dans le menu "tools",
le renommer en "make obsolete"
* DONE Check if remark in doc/api.tex line 80 is still valid (A)
* DONE put an up-to-date use_api.ml in the manual (C)
* DONE enlever les caracteres de tab des sources
......
......@@ -80,9 +80,10 @@ As expected, the output is as follows.
\begin{verbatim}
formula 2 is: A /\ B -> A
\end{verbatim}
\todo{Check: Notice that the concrete syntax of \why forbids predicate identifiers
to start with a capital letter. This constraint does not exist when
building those directly using library calls.}
Notice that the concrete syntax of \why forbids function and predicate
names to start with a capital letter (except for the algebraic type
constructors which must start with one). This constraint is not enforced
when building those directly using library calls.
\section{Building Tasks}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment