diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 17:03:24 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 17:03:24 +0100 |
| commit | bdaa3eb0ad6486186519ba1ba574e8ac92505cf0 (patch) | |
| tree | 317a87bfe26b092294e24e1e2c38199e1a7cc54d /mppa_k1c/Asmblockgen.v | |
| parent | b873e06abcee1c7f6a51aaabb973b550a52a5b61 (diff) | |
| download | compcert-kvx-bdaa3eb0ad6486186519ba1ba574e8ac92505cf0.tar.gz compcert-kvx-bdaa3eb0ad6486186519ba1ba574e8ac92505cf0.zip | |
Mise à jour vis à vis de CompCert 3.4
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 2ac5cc16..d024a74f 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -62,6 +62,7 @@ Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativ Notation "a ::i b" := (cons (A:=basic) a b) (at level 49, right associativity). Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associativity). Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity). +Notation "a @@ b" := (app a b) (at level 49, right associativity). (** Smart constructors for arithmetic operations involving a 32-bit or 64-bit integer constant. Depending on whether the @@ -910,7 +911,7 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: | mb :: lmb => do lb <- transl_block f mb (if Machblock.header mb then ep else false); do lb' <- transl_blocks f lmb false; - OK (lb ++ lb') + OK (lb @@ lb') end . |