WhyML documentation: old/at, evaluation order

Makefile.in

@@ -1218,7 +1218,7 @@ ifeq (@enable_doc@,yes)
 doc: doc/manual.pdf doc/html/index.html
 
 BNF = qualid label constant operator term type formula theory theory2 \
-	why_file spec expr expr2 module whyml_file
+	why_file spec expr expr2 module whyml_file term_old_at
 BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
 
 doc/%_bnf.tex: doc/%.bnf doc/bnf

doc/syntaxref.tex

@@ -179,6 +179,13 @@ is given in Figure~\ref{fig:bnf:spec}.
   \caption{Specification clauses in programs.}
 \label{fig:bnf:spec}
 \end{figure}
+Within specifications, terms are extended with new constructs
+\verb|old| and \verb|at|:
+\begin{center}\framebox{\input{./term_old_at_bnf.tex}}\end{center}
+Within a postcondition, $\verb|old|~t$ refers to the value of term $t$
+in the prestate. Within the scope of a code mark $L$,
+the term $\verb|at|~t~\verb|'|L$ refers to the value of term $t$ at the program
+point corresponding to $L$.
 
 \subsection{Expressions}
 
@@ -196,6 +203,12 @@ Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}.
 \label{fig:bnf:exprb}
 \end{figure}
 
+In applications, arguments are evaluated from right to left.
+This includes applications of infix operators, with the only exception of
+lazy operators \verb|&&| and \verb+||+ that evaluate from left to
+right, lazily.
+
+
 % In the following we describe the informal semantics of each
 % constructs, and provide the corresponding rule for computing the
 % weakest precondition.

doc/term_old_at.bnf

+\begin{syntax}
+  term ::= ...                    ;
+       | "old" term		  ;
+       | "at" term "'" uident	  ;
+\end{syntax}