From 8dfd1db5c496821b8cb94ce7b121e4b9bba3d265 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 7 Dec 2020 23:51:58 +0100 Subject: Some cleanup in todos --- aarch64/Asmblockgen.v | 12 ------------ 1 file changed, 12 deletions(-) (limited to 'aarch64/Asmblockgen.v') 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). -- cgit