aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Tailcall.v
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 08:19:32 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 08:19:32 +0100
commit0d471625d7613a72c0bb8519e0427f971b53b35f (patch)
tree7478569a4118ff0cf851f8d491d628aa78454955 /backend/Tailcall.v
parentbc5b28ec16590c52da2772b1cc296247ccf528c1 (diff)
parent3bdb983e0b21c8d45e85aff08278475396038f4f (diff)
downloadcompcert-kvx-0d471625d7613a72c0bb8519e0427f971b53b35f.tar.gz
compcert-kvx-0d471625d7613a72c0bb8519e0427f971b53b35f.zip
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'backend/Tailcall.v')
-rw-r--r--backend/Tailcall.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 939abeea..b7a62d74 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -82,7 +82,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) :=
| Icall sig ros args res s =>
if is_return niter f s res
&& tailcall_is_possible sig
- && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res)
+ && rettype_eq sig.(sig_res) f.(fn_sig).(sig_res)
then Itailcall sig ros args
else instr
| _ => instr