diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index d15bc90ad4..16a73e12f8 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -98,6 +98,7 @@ Inductive statement : Type :=
   | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *)
   | Sset : ident -> expr -> statement   (**r assignment [tempvar = rvalue] *)
   | Scall: option ident -> expr -> list expr -> statement (**r function call *)
+  | Stailcall: expr -> list expr -> statement (**r function call in tail position *)
   | Sbuiltin: option ident -> external_function -> typelist -> list expr -> statement (**r builtin invocation *)
   | Ssequence : statement -> statement -> statement  (**r sequence *)
   | Sifthenelse : expr  -> statement -> statement -> statement (**r conditional *)
@@ -580,6 +581,17 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid a al) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
+  | step_tailcall:   forall f a al k e le m tyargs tyres cconv vf vargs fd m',
+      classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
+      eval_expr e le m a vf ->
+      eval_exprlist e le m al tyargs vargs ->
+      Genv.find_funct ge vf = Some fd ->
+      type_of_fundef fd = Tfunction tyargs tyres cconv ->
+      fn_return f = tyres ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
+      step (State f (Stailcall a al) k e le m)
+        E0 (Callstate fd vargs (call_cont k) m')
+
   | step_builtin:   forall f optid ef tyargs al k e le m vargs t vres m',
       eval_exprlist e le m al tyargs vargs ->
       external_call ef ge vargs m t vres m' ->
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 1b031866e8..8f4d44e9b0 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -164,6 +164,10 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
       do te <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
       OK (Scall optid sig te tel)
+  | Csharpminor.Stailcall sig e el =>
+      do te <- transl_expr cenv e;
+      do tel <- transl_exprlist cenv el;
+      OK (Stailcall sig te tel)
   | Csharpminor.Sbuiltin optid ef el =>
       do tel <- transl_exprlist cenv el;
       OK (Sbuiltin optid ef tel)
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index bc1c92ca7c..5f77a44efd 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1664,6 +1664,12 @@ Proof.
   econstructor; split. apply star_refl. split. exact I. econstructor; eauto.
 Qed.
 
+Lemma call_cont_is_call_cont:
+  forall k, Csharpminor.is_call_cont (Csharpminor.call_cont k).
+Proof.
+  induction k; simpl; auto.
+Qed.
+
 (** Properties of [switch] compilation *)
 
 Inductive lbl_stmt_tail: lbl_stmt -> nat -> lbl_stmt -> Prop :=
@@ -1951,7 +1957,7 @@ Lemma transl_step_correct:
 Proof.
   induction 1; intros T1 MSTATE; inv MSTATE.
 
-(* skip seq *)
+- (* skip seq *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -1963,7 +1969,7 @@ Proof.
   exploit IHMK; eauto. intros [T2 [A B]].
   exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq.
   auto.
-(* skip block *)
+- (* skip block *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -1972,7 +1978,7 @@ Proof.
   exploit IHMK; eauto. intros [T2 [A B]].
   exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq.
   auto.
-(* skip call *)
+- (* skip call *)
   monadInv TR. left.
   exploit match_is_call_cont; eauto. intros [tk' [A [B C]]].
   exploit match_callstack_freelist; eauto. intros [tm' [P [Q R]]].
@@ -1980,7 +1986,7 @@ Proof.
   eapply plus_right. eexact A. apply step_skip_call. auto. eauto. traceEq.
   econstructor; eauto.
 
-(* set *)
+- (* set *)
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   left; econstructor; split.
@@ -1988,7 +1994,7 @@ Proof.
   econstructor; eauto.
   eapply match_callstack_set_temp; eauto.
 
-(* store *)
+- (* store *)
   monadInv TR.
   exploit transl_expr_correct. eauto. eauto. eexact H. eauto.
   intros [tv1 [EVAL1 VINJ1]].
@@ -2005,7 +2011,7 @@ Proof.
   intros. eapply Mem.perm_store_2; eauto.
   intros. eapply Mem.perm_store_1; eauto.
 
-(* call *)
+- (* call *)
   simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]].
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]].
@@ -2022,7 +2028,24 @@ Proof.
   eapply match_Kcall with (cenv' := cenv); eauto.
   red; auto.
 
-(* builtin *)
+- (* tailcall *)
+  simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]].
+  monadInv TR.
+  exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]].
+  assert (tvf = vf).
+    exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
+    eapply val_inject_function_pointer; eauto.
+  subst tvf.
+  exploit transl_exprlist_correct; eauto. intros [tvargs [EVAL2 VINJ2]].
+  exploit match_callstack_freelist; eauto. intros [tm' [P [Q R]]].
+  left; econstructor; split.
+  apply plus_one. eapply step_tailcall; eauto.
+  apply sig_preserved; eauto.
+  econstructor; eauto.
+  eapply match_call_cont; eauto.
+  apply call_cont_is_call_cont.
+
+- (* builtin *)
   monadInv TR.
   exploit transl_exprlist_correct; eauto.
   intros [tvargs [EVAL2 VINJ2]].
@@ -2048,37 +2071,37 @@ Opaque PTree.set.
   eapply match_callstack_set_temp; eauto.
   auto.
 
-(* seq *)
+- (* seq *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
   econstructor; eauto.
-(* seq 2 *)
+- (* seq 2 *)
   right. split. auto. split. auto. econstructor; eauto.
 
-(* ifthenelse *)
+- (* ifthenelse *)
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Ptrofs.zero) te tm); split.
   apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto.
   econstructor; eauto. destruct b; auto.
 
-(* loop *)
+- (* loop *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
   econstructor; eauto. simpl. rewrite EQ; auto.
 
-(* block *)
+- (* block *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
   econstructor; eauto.
 
-(* exit seq *)
+- (* exit seq *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -2090,7 +2113,7 @@ Opaque PTree.set.
   exists T2; split; auto. eapply plus_left.
   simpl. constructor. apply plus_star; eauto. traceEq.
 
-(* exit block 0 *)
+- (* exit block 0 *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -2100,7 +2123,7 @@ Opaque PTree.set.
   exists T2; split; auto. simpl.
   eapply plus_left. constructor. apply plus_star; eauto. traceEq.
 
-(* exit block n+1 *)
+- (* exit block n+1 *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -2110,7 +2133,7 @@ Opaque PTree.set.
   exists T2; split; auto. simpl.
   eapply plus_left. constructor. apply plus_star; eauto. traceEq.
 
-(* switch *)
+- (* switch *)
   simpl in TR. destruct (switch_table cases O) as [tbl dfl] eqn:STBL. monadInv TR.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   assert (SA: switch_argument islong tv n).
@@ -2129,15 +2152,14 @@ Opaque PTree.set.
   reflexivity. reflexivity. traceEq.
   auto.
 
-(* return none *)
+- (* return none *)
   monadInv TR. left.
   exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
   econstructor; split.
   apply plus_one. eapply step_return_0. eauto.
   econstructor; eauto. eapply match_call_cont; eauto.
-  simpl; auto.
 
-(* return some *)
+- (* return some *)
   monadInv TR. left.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
@@ -2145,13 +2167,13 @@ Opaque PTree.set.
   apply plus_one. eapply step_return_1. eauto. eauto.
   econstructor; eauto. eapply match_call_cont; eauto.
 
-(* label *)
+- (* label *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
 
-(* goto *)
+- (* goto *)
   monadInv TR.
   exploit transl_find_label_body; eauto.
   intros [ts' [tk' [xenv' [A [B C]]]]].
@@ -2159,7 +2181,7 @@ Opaque PTree.set.
   apply plus_one. apply step_goto. eexact A.
   econstructor; eauto.
 
-(* internal call *)
+- (* internal call *)
   monadInv TR. generalize EQ; clear EQ; unfold transl_function.
   caseEq (build_compilenv f). intros ce sz BC.
   destruct (zle sz Ptrofs.max_unsigned); try congruence.
@@ -2178,7 +2200,7 @@ Opaque PTree.set.
   econstructor. eexact TRBODY. eauto. eexact MINJ2. eexact MCS2.
   inv MK; simpl in ISCC; contradiction || econstructor; eauto.
 
-(* external call *)
+- (* external call *)
   monadInv TR.
   exploit match_callstack_match_globalenvs; eauto. intros [hi MG].
   exploit external_call_mem_inject; eauto.
@@ -2195,7 +2217,7 @@ Opaque PTree.set.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
-(* return *)
+- (* return *)
   inv MK. simpl.
   left; econstructor; split.
   apply plus_one. econstructor; eauto.
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 4393640ced..c4260882da 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -62,6 +62,7 @@ Inductive stmt : Type :=
   | Sset : ident -> expr -> stmt
   | Sstore : memory_chunk -> expr -> expr -> stmt
   | Scall : option ident -> signature -> expr -> list expr -> stmt
+  | Stailcall: signature -> expr -> list expr -> stmt
   | Sbuiltin : option ident -> external_function -> list expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: expr -> stmt -> stmt -> stmt
@@ -390,6 +391,15 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid sig a bl) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
+  | step_tailcall: forall f sig a bl k e le m vf vargs fd m',
+      eval_expr e le m a vf ->
+      eval_exprlist e le m bl vargs ->
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
+      step (State f (Stailcall sig a bl) k e le m)
+        E0 (Callstate fd vargs (call_cont k) m')
+
   | step_builtin: forall f optid ef bl k e le m vargs t vres m',
       eval_exprlist e le m bl vargs ->
       external_call ef ge vargs m t vres m' ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 9e80417667..5fb302abe2 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -687,6 +687,17 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
           OK (make_funcall x res sg tb tcl)
       | _ => Error(msg "Cshmgen.transl_stmt(call)")
       end
+  | Clight.Stailcall b cl =>
+      match classify_fun (typeof b) with
+      | fun_case_f args res cconv =>
+          do tb <- transl_expr ce b;
+          do tcl <- transl_arglist ce cl args;
+          let sg := {| sig_args := typlist_of_arglist cl args;
+                       sig_res  := rettype_of_type res;
+                       sig_cc   := cconv |} in
+          OK (Stailcall sg tb tcl)
+      | _ => Error(msg "Cshmgen.transl_stmt(tailcall)")
+      end
   | Clight.Sbuiltin x ef tyargs bl =>
       do tbl <- transl_arglist ce bl tyargs;
       OK(Sbuiltin x ef tbl)
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 9829388805..2c32ff3edc 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1572,6 +1572,9 @@ Proof.
   simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
   unfold make_funcall.
   destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto.
+- (* tailcall *)
+  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
+  auto.
 - (* builtin *)
   auto.
 - (* seq *)
@@ -1651,6 +1654,12 @@ Proof.
   split; auto; eapply match_Kcall_normalize; eauto.
 Qed.
 
+Lemma call_cont_is_call_cont:
+  forall k, Clight.is_call_cont (Clight.call_cont k).
+Proof.
+  induction k; simpl; auto.
+Qed.
+
 (** The simulation proof *)
 
 Lemma transl_step:
@@ -1725,6 +1734,26 @@ Proof.
     intros. eapply make_normalization_correct; eauto. constructor; eauto.
     exact I.
 
+- (* tailcall *)
+  revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
+  intros targs tres cc CF TR. monadInv TR. inv MTR.
+  exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
+  rewrite H in CF. simpl in CF. inv CF.
+  set (sg := {| sig_args := typlist_of_arglist al targs;
+                sig_res := rettype_of_type (fn_return f);
+                sig_cc := cc |}) in *.
+  assert (SIG: funsig tfd = sg).
+  { unfold sg; erewrite typlist_of_arglist_eq by eauto.
+    eapply transl_fundef_sig1; eauto. rewrite H3; auto. }
+  econstructor; split.
+  apply plus_one. eapply step_tailcall; eauto.
+  eapply transl_expr_correct with (cunit := cu); eauto.
+  eapply transl_arglist_correct with (cunit := cu); eauto.
+  eapply match_env_free_blocks; eauto.
+  eapply match_callstate with (ce := prog_comp_env cu); eauto.
+  eapply match_cont_call_cont. eauto.
+  apply call_cont_is_call_cont.
+
 - (* builtin *)
   monadInv TR. inv MTR.
   econstructor; split.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index a9ecb342cd..a226bd2caa 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -143,6 +143,10 @@ let rec print_stmt p s =
                 (temp_name id)
                 expr (15, e1)
                 print_expr_list (true, el)
+  | Stailcall(e1, el) ->
+      fprintf p "@[<hv 2>return %a@,(@[<hov 0>%a@]);@ /*tailcall*/@]"
+                expr (15, e1)
+                print_expr_list (true, el)
   | Sbuiltin(None, ef, tyargs, el) ->
       fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]"
                 (name_of_external ef)
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 0a164e2949..750658ac53 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -119,6 +119,8 @@ Fixpoint simpl_stmt (cenv: compilenv) (s: statement) : res statement :=
   | Scall optid a al =>
       do x <- check_opttemp cenv optid;
       OK (Scall optid (simpl_expr cenv a) (simpl_exprlist cenv al))
+  | Stailcall a al =>
+      OK (Stailcall (simpl_expr cenv a) (simpl_exprlist cenv al))
   | Sbuiltin optid ef tyargs al =>
       do x <- check_opttemp cenv optid;
       OK (Sbuiltin optid ef tyargs (simpl_exprlist cenv al))
@@ -208,6 +210,7 @@ Fixpoint addr_taken_stmt (s: statement) : VSet.t :=
   | Sassign a b => VSet.union (addr_taken_expr a) (addr_taken_expr b)
   | Sset id a => addr_taken_expr a
   | Scall optid a bl => VSet.union (addr_taken_expr a) (addr_taken_exprlist bl)
+  | Stailcall a bl => VSet.union (addr_taken_expr a) (addr_taken_exprlist bl)
   | Sbuiltin optid ef tyargs bl => addr_taken_exprlist bl
   | Ssequence s1 s2 => VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2)
   | Sifthenelse a s1 s2 =>
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index c133d8eab7..760b433bc0 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1952,6 +1952,8 @@ Proof.
   monadInv TS; auto.
   (* call *)
   monadInv TS; auto.
+  (* tailcall *)
+  monadInv TS; auto.
   (* builtin *)
   monadInv TS; auto.
   (* seq *)
@@ -2035,7 +2037,7 @@ Lemma step_simulation:
 Proof.
   induction 1; simpl; intros; inv MS; simpl in *; try (monadInv TRS).
 
-(* assign *)
+- (* assign *)
   generalize (is_liftable_var_charact (cenv_for f) a1); destruct (is_liftable_var (cenv_for f) a1) as [id|]; monadInv TRS.
   (* liftable *)
   intros [ty [P Q]]; subst a1; simpl in *.
@@ -2043,7 +2045,7 @@ Proof.
   exploit sem_cast_inject; eauto. intros [tv [C D]].
   exploit me_vars; eauto. instantiate (1 := id). intros MV.
   inv H.
-  (* local variable *)
++ (* local variable *)
   econstructor; split.
   eapply step_Sset_debug. eauto. rewrite typeof_simpl_expr. eauto.
   econstructor; eauto with compat.
@@ -2052,9 +2054,9 @@ Proof.
   inv MV; try congruence. inv H2; try congruence. unfold Mem.storev in H3.
   eapply Mem.store_unmapped_inject; eauto. congruence.
   erewrite assign_loc_nextblock; eauto.
-  (* global variable *)
++ (* global variable *)
   inv MV; congruence.
-  (* not liftable *)
++ (* not liftable *)
   intros P.
   exploit eval_simpl_lvalue; eauto with compat. intros [tb [tofs [E F]]].
   exploit eval_simpl_expr; eauto with compat. intros [tv2 [A B]].
@@ -2069,14 +2071,14 @@ Proof.
   erewrite assign_loc_nextblock; eauto.
   erewrite assign_loc_nextblock; eauto.
 
-(* set temporary *)
+- (* set temporary *)
   exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
   econstructor; split.
   apply plus_one. econstructor. eauto.
   econstructor; eauto with compat.
   eapply match_envs_set_temp; eauto.
 
-(* call *)
+- (* call *)
   exploit eval_simpl_expr; eauto with compat. intros [tvf [A B]].
   exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]].
   exploit match_cont_find_funct; eauto. intros [tfd [P Q]].
@@ -2088,7 +2090,22 @@ Proof.
   econstructor; eauto.
   intros. econstructor; eauto.
 
-(* builtin *)
+- (* tailcall *)
+  exploit eval_simpl_expr; eauto with compat. intros [tvf [A B]].
+  exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]].
+  exploit match_cont_find_funct; eauto. intros [tfd [P Q]].
+  exploit match_envs_free_blocks; eauto. intros [tm' [U V]].
+  econstructor; split.
+  apply plus_one. eapply step_tailcall with (fd := tfd).
+  rewrite typeof_simpl_expr. eauto.
+  eauto. eauto. eauto.
+  erewrite type_of_fundef_preserved; eauto.
+  monadInv TRF; auto.
+  eauto.
+  econstructor; eauto.
+  intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto.
+
+- (* builtin *)
   exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]].
   exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat.
   intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
@@ -2102,53 +2119,53 @@ Proof.
   eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
   eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
 
-(* sequence *)
+- (* sequence *)
   econstructor; split. apply plus_one. econstructor.
   econstructor; eauto with compat. econstructor; eauto with compat.
 
-(* skip sequence *)
+- (* skip sequence *)
   inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.
 
-(* continue sequence *)
+- (* continue sequence *)
   inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.
 
-(* break sequence *)
+- (* break sequence *)
   inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.
 
-(* ifthenelse *)
+- (* ifthenelse *)
   exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
   econstructor; split.
   apply plus_one. apply step_ifthenelse with (v1 := tv) (b := b). auto.
   rewrite typeof_simpl_expr. eapply bool_val_inject; eauto.
   destruct b; econstructor; eauto with compat.
 
-(* loop *)
+- (* loop *)
   econstructor; split. apply plus_one. econstructor. econstructor; eauto with compat. econstructor; eauto with compat.
 
-(* skip-or-continue loop *)
+- (* skip-or-continue loop *)
   inv MCONT. econstructor; split.
   apply plus_one. econstructor. destruct H; subst x; simpl in *; intuition congruence.
   econstructor; eauto with compat. econstructor; eauto with compat.
 
-(* break loop1 *)
+- (* break loop1 *)
   inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop1.
   econstructor; eauto.
 
-(* skip loop2 *)
+- (* skip loop2 *)
   inv MCONT. econstructor; split. apply plus_one. eapply step_skip_loop2.
   econstructor; eauto with compat. simpl; rewrite H2; rewrite H4; auto.
 
-(* break loop2 *)
+- (* break loop2 *)
   inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop2.
   econstructor; eauto.
 
-(* return none *)
+- (* return none *)
   exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
   econstructor; split. apply plus_one. econstructor; eauto.
   econstructor; eauto.
   intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto.
 
-(* return some *)
+- (* return some *)
   exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
   exploit sem_cast_inject; eauto. intros [tv' [C D]].
   exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
@@ -2157,7 +2174,7 @@ Proof.
   econstructor; eauto.
   intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto.
 
-(* skip call *)
+- (* skip call *)
   exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
   econstructor; split. apply plus_one. econstructor; eauto.
   eapply match_cont_is_call_cont; eauto.
@@ -2165,7 +2182,7 @@ Proof.
   econstructor; eauto.
   intros. apply match_cont_change_cenv with (cenv_for f); auto. eapply match_cont_free_env; eauto.
 
-(* switch *)
+- (* switch *)
   exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
   econstructor; split. apply plus_one. econstructor; eauto.
   rewrite typeof_simpl_expr. instantiate (1 := n).
@@ -2178,20 +2195,20 @@ Proof.
   econstructor; eauto. rewrite addr_taken_seq_of_labeled_statement.
   apply compat_cenv_select_switch. eauto with compat.
 
-(* skip-break switch *)
+- (* skip-break switch *)
   inv MCONT. econstructor; split.
   apply plus_one. eapply step_skip_break_switch. destruct H; subst x; simpl in *; intuition congruence.
   econstructor; eauto with compat.
 
-(* continue switch *)
+- (* continue switch *)
   inv MCONT. econstructor; split.
   apply plus_one. eapply step_continue_switch.
   econstructor; eauto with compat.
 
-(* label *)
+- (* label *)
   econstructor; split. apply plus_one. econstructor. econstructor; eauto.
 
-(* goto *)
+- (* goto *)
   generalize TRF; intros TRF'. monadInv TRF'.
   exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x (call_cont tk)).
     eauto. eapply match_cont_call_cont. eauto.
@@ -2202,7 +2219,7 @@ Proof.
   rewrite find_label_add_debug_params. rewrite find_label_store_params. rewrite find_label_add_debug_vars. eexact A.
   econstructor; eauto.
 
-(* internal function *)
+- (* internal function *)
   monadInv TRFD. inv H.
   generalize EQ; intro EQ'; monadInv EQ'.
   assert (list_norepet (var_names (fn_params f ++ fn_vars f))).
@@ -2248,7 +2265,7 @@ Proof.
   rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). extlia.
   rewrite T; extlia.
 
-(* external function *)
+- (* external function *)
   monadInv TRFD. inv FUNTY.
   exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals.
   eapply match_cont_globalenv. eexact (MCONT VSet.empty).
@@ -2261,7 +2278,7 @@ Proof.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
-(* return *)
+- (* return *)
   specialize (MCONT (cenv_for f)). inv MCONT.
   econstructor; split.
   apply plus_one. econstructor.
diff --git a/export/Clightnorm.ml b/export/Clightnorm.ml
index 88d44c08a9..9a7a8872cf 100644
--- a/export/Clightnorm.ml
+++ b/export/Clightnorm.ml
@@ -118,6 +118,10 @@ let rec norm_stmt s =
       let (sl1, e') = norm_expr e in
       let (sl2, el') = norm_expr_list el in
       add_sequence (sl1 @ sl2) (Scall(optid, e', el'))  
+  | Stailcall(e, el) ->
+      let (sl1, e') = norm_expr e in
+      let (sl2, el') = norm_expr_list el in
+      add_sequence (sl1 @ sl2) (Stailcall(e', el'))  
   | Sbuiltin(optid, ef, tyl, el) ->
       let (sl, el') = norm_expr_list el in
       add_sequence sl (Sbuiltin(optid, ef, tyl, el'))
diff --git a/export/ExportClight.ml b/export/ExportClight.ml
index e3b00986a9..2d6f9b203d 100644
--- a/export/ExportClight.ml
+++ b/export/ExportClight.ml
@@ -95,6 +95,9 @@ let rec stmt p = function
   | Scall(optid, e1, el) ->
       fprintf p "@[<hov 2>(Scall %a@ %a@ %a)@]"
         (print_option ident) optid expr e1 (print_list expr) el
+  | Stailcall(e1, el) ->
+      fprintf p "@[<hov 2>(Stailcall@ %a@ %a)@]"
+        expr e1 (print_list expr) el
   | Sbuiltin(optid, ef, tyl, el) ->
       fprintf p "@[<hov 2>(Sbuiltin %a@ %a@ %a@ %a)@]"
         (print_option ident) optid
@@ -197,6 +200,8 @@ let rec name_stmt = function
   | Sset(id, e2) -> name_temporary id; name_expr e2
   | Scall(optid, e1, el) ->
       name_opt_temporary optid; name_expr e1; List.iter name_expr el
+  | Stailcall(e1, el) ->
+      name_expr e1; List.iter name_expr el
   | Sbuiltin(optid, ef, tyl, el) ->
       name_opt_temporary optid; List.iter name_expr el
   | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2