From 9cc12b684ee6833971c9549aa76cc683ba931090 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:08:07 +0200 Subject: begin scripting the Compiler.v file --- backend/Unusedglob.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Unusedglob.v') diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 93ca7af4..3b8e19ad 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -126,7 +126,7 @@ Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef u Definition global_defined (p: program) (pm: prog_map) (id: ident) : bool := match pm!id with Some _ => true | None => ident_eq id (prog_main p) end. -Definition transform_program (p: program) : res program := +Definition transf_program (p: program) : res program := let pm := prog_defmap p in match used_globals p pm with | None => Error (msg "Unusedglob: analysis failed") -- cgit