Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1 insertions, 0 deletions

diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll
index ae71e0c1..7951982f 100644
--- a/caml/CMlexer.mll
+++ b/caml/CMlexer.mll
@@ -99,6 +99,7 @@ rule token = parse
   | "*" { STAR }
   | "*f"    { STARF }
   | "switch"    { SWITCH }
+  | "tailcall"  { TAILCALL }
   | "~"    { TILDE }
   | "var"    { VAR }
   | "void"    { VOID }