diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-04 17:53:21 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:59:07 +0200 |
| commit | 1412a262c0bb95ebc78ac7c4d79e0fa81954c82a (patch) | |
| tree | 1b5dca24847b29b1a5129f2f1a0b0b1eededa566 /mppa_k1c/Asmblockgen.v | |
| parent | d1c08acee2c3aca35a2dd31b69f7cde852069f6c (diff) | |
| download | compcert-kvx-1412a262c0bb95ebc78ac7c4d79e0fa81954c82a.tar.gz compcert-kvx-1412a262c0bb95ebc78ac7c4d79e0fa81954c82a.zip | |
Asmblock -> Asm presque fini.. erreur sur driver/Compiler.v
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index f9f38b18..4bb23e8e 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -838,7 +838,7 @@ Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_ otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) -Obligation Tactic := bblock_auto_correct. +Local Obligation Tactic := bblock_auto_correct. Program Definition gen_bblock_noctl (hd: list label) (c: list basic) := match c with |