From 60e4ad85c6cd433c9e28c9e407a957ca3a302c22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 18:00:14 +0200 Subject: CSE3: better builtin handling --- backend/CSE2.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index cad740ba..8e2307b0 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -262,7 +262,7 @@ Definition load (chunk: memory_chunk) (addr : addressing) | None => load1 chunk addr dst args rel end. -Fixpoint kill_builtin_res res rel := +Definition kill_builtin_res res rel := match res with | BR r => kill_reg r rel | _ => rel -- cgit