diff options
| author | glondu | 2008-05-05 15:09:38 +0000 |
|---|---|---|
| committer | glondu | 2008-05-05 15:09:38 +0000 |
| commit | 64a4b9851f49f5c0d859d60def1f1de8e9549a9d (patch) | |
| tree | 41aac5cd287c31ecfb969b3a5e8965533aaa6b1b | |
| parent | af8e8176a6ca63c59621e4775d50faf51627b4cc (diff) | |
Minor updates in the documentation of notations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10886 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index dcac68f1a1..9f607f05e4 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -73,7 +73,7 @@ Consider for example the new notation Notation "A \/ B" := (or A B). \end{coq_example*} -Clearly, an expression such as {\tt (A:Prop)True \verb=/\= A \verb=\/= +Clearly, an expression such as {\tt forall A:Prop, True \verb=/\= A \verb=\/= A \verb=\/= False} is ambiguous. To tell the {\Coq} parser how to interpret the expression, a priority between the symbols \verb=/\= and \verb=\/= has to be given. Assume for instance that we want conjunction @@ -179,7 +179,7 @@ See the next section for more about factorization. \subsection{Simple factorization rules} -{\Coq} extensible parsing is performed by Camlp4 which is essentially a +{\Coq} extensible parsing is performed by Camlp5 which is essentially a LL1 parser. Hence, some care has to be taken not to hide already existing rules by new rules. Some simple left factorization work has to be done. Here is an example. |