diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-07 23:51:58 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-07 23:51:58 +0100 |
| commit | 8dfd1db5c496821b8cb94ce7b121e4b9bba3d265 (patch) | |
| tree | f15db31de0783d499a88ae6a4a6920202d9b9472 /aarch64/Asmblockgen.v | |
| parent | a44c77d4f36894f11958f29a738e791c069cd2e0 (diff) | |
| download | compcert-kvx-8dfd1db5c496821b8cb94ce7b121e4b9bba3d265.tar.gz compcert-kvx-8dfd1db5c496821b8cb94ce7b121e4b9bba3d265.zip | |
Some cleanup in todos
Diffstat (limited to 'aarch64/Asmblockgen.v')
| -rw-r--r-- | aarch64/Asmblockgen.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 137b5871..fbbf7507 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -157,18 +157,6 @@ Program Definition insert_basic (bi: basic) (k:bblocks): bblocks := Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity). -(* TODO: Coercions to move in Asmblock ? *) -Coercion PArithP: arith_p >-> Funclass. -Coercion PArithPP: arith_pp >-> Funclass. -Coercion PArithPPP: arith_ppp >-> Funclass. -Coercion PArithRR0: arith_rr0 >-> Funclass. -Coercion PArithRR0R: arith_rr0r >-> Funclass. -Coercion PArithARRRR0: arith_arrrr0 >-> Funclass. -Coercion PArithComparisonP: arith_comparison_p >-> Funclass. -Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass. -Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass. -Coercion PArith: ar_instruction >-> basic. - (* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *) (** Alignment check for symbols *) Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity). |