diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-11-16 16:40:22 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-11-16 16:40:22 +0100 |
commit | 9117e139d6aad064756f58427ec137d8bb787fcc (patch) | |
tree | ca018f5d28795244d2da9b3dcd12935a118fa59e /backend | |
parent | 09eed5e98d88260942d7860aec983c539faeac35 (diff) | |
download | compcert-kvx-9117e139d6aad064756f58427ec137d8bb787fcc.tar.gz compcert-kvx-9117e139d6aad064756f58427ec137d8bb787fcc.zip |
minor fix in coq2html comment
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Tunneling.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/Tunneling.v b/backend/Tunneling.v index bb1ac9f5..269ebb6f 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -54,7 +54,8 @@ Naively, we may define [branch_t f pc] as follows: L1: nop L1; >> or -<< L1: nop L2; +<< + L1: nop L2; L2: nop L1; >> Coq warns us of this fact by not accepting the definition |