From f0a5038b4e4220300637d3e9e918d9ec31623108 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Oct 2015 15:33:47 +0200 Subject: Added versions of the tranform_* functions in AST to work with functions taking the ident as argument. This functions are currently not used inside the proven part but it is nice to have them already there, when they are used by some future pass. They also come equiped with the corresponding proofs. --- arm/Asmexpand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/Asmexpand.ml') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index d13015ff..da08bf7c 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -403,7 +403,7 @@ let expand_function fn = with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) -let expand_fundef = function +let expand_fundef _ = function | Internal f -> begin match expand_function f with | Errors.OK tf -> Errors.OK (Internal tf) @@ -413,4 +413,4 @@ let expand_fundef = function Errors.OK (External ef) let expand_program (p: Asm.program) : Asm.program Errors.res = - AST.transform_partial_program expand_fundef p + AST.transform_partial_ident_program expand_fundef p -- cgit