Commit 727969d5 authored by POTTIER Francois's avatar POTTIER Francois

Doc: fixed the name of the theorem [Parser.unambiguous].

parent 3306d160
......@@ -2069,8 +2069,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
named \verb+Parser.unambiguous+.
% 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