From 4df03aaf5204d2f15885b49fe3f5c9cb61b4596d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Feb 2021 18:31:46 +0100 Subject: Ccompu expansion --- riscV/Asmgenproof.v | 1 + 1 file changed, 1 insertion(+) (limited to 'riscV/Asmgenproof.v') diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 8aa3d3b2..369b8280 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -295,6 +295,7 @@ Opaque Int.eq. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. +- destruct optR0 as [[]|]; simpl; TailNoLabel. Qed. Remark indexed_memory_access_label: -- cgit