diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:33:32 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:33:32 +0000 |
| commit | adc9e990a0c338cef57ff1bd9717adcc781f283c (patch) | |
| tree | cdbb1265be6c524ade10565b1a2b500b510f3491 /papers/cfrontend_new/trace.etex | |
| parent | 355b4abcee015c3fae9ac5653c25259e104a886c (diff) | |
| download | compcert-adc9e990a0c338cef57ff1bd9717adcc781f283c.tar.gz compcert-adc9e990a0c338cef57ff1bd9717adcc781f283c.zip | |
Deplacement du repertoire "papers" dans la hierarchie SVN
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'papers/cfrontend_new/trace.etex')
| -rw-r--r-- | papers/cfrontend_new/trace.etex | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/papers/cfrontend_new/trace.etex b/papers/cfrontend_new/trace.etex deleted file mode 100644 index d02b1fe9..00000000 --- a/papers/cfrontend_new/trace.etex +++ /dev/null @@ -1,19 +0,0 @@ -\begin{figure} - -\begin{syntax} -\syntaxclass{Event values:} -\evv & ::= & n & integer value\\ - & \alt & f & floating-point value -% -\syntaxclass{Events:} -\ev & ::= & \id \, \evv^* \, \evv & -% -\syntaxclass{Execution traces:} -\tr & ::= & \E0 & empty trace \\ - & \alt & [\ev] & external call \\ - & \alt & \cat \tr \tr& concatenation -\end{syntax} -\caption{Execution traces} -\label{fig:trace} -\end{figure} - |