diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-08 15:33:47 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-08 15:33:47 +0200 |
| commit | f0a5038b4e4220300637d3e9e918d9ec31623108 (patch) | |
| tree | 2d1e5f006d7a9bcd4c2a1ddcf5803be97b105db9 /arm/Asmexpand.ml | |
| parent | ed1f32134283d3cd4f939a26dfd99992ec48da86 (diff) | |
| download | compcert-kvx-f0a5038b4e4220300637d3e9e918d9ec31623108.tar.gz compcert-kvx-f0a5038b4e4220300637d3e9e918d9ec31623108.zip | |
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.
Diffstat (limited to 'arm/Asmexpand.ml')
| -rw-r--r-- | arm/Asmexpand.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |