Commit 8520f906 authored by POTTIER Francois's avatar POTTIER Francois

TODO item.

parent 6cac6f12
......@@ -30,6 +30,9 @@
revenu, on peut examiner les items de l'état courant et donner des
positions de début d'item qui devraient être intéressantes.
* bundle the Coq library with menhir, and add demos/calc-coq
to show how it is used
* Clarifier si ocamlbuild doit recevoir -use-ocamlfind, -no-ocamlfind,
ou rien; tester en particulier sous Windows?
......
......@@ -2051,6 +2051,7 @@ grammar), then (given sufficient fuel) it is accepted by the parser.
These results imply that the grammar is unambiguous: for every input, there is
at most one valid interpretation. This is proved by another generated theorem,
named \verb+unambiguous+.
% TEMPORARY clarifier où est ce théorème et comment il s'appelle
% jh: Pas besoin de prouver la terminaison pour avoir la non-ambiguïté, car
% les cas de non-terminaison ne concernent que les entrées invalides.
......
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