diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 15:07:47 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 15:07:47 +0100 |
commit | 272a5b812b72f4c3e409ccdbeaf3476d95c4b552 (patch) | |
tree | 6a8d5e75a11860b69522cef3b512b1ef5effb438 /backend/CMparser.mly | |
parent | 2185164c1845c30ebd4118ed5bc8d339b16663a9 (diff) | |
download | compcert-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.tar.gz compcert-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.zip |
Deactivate warning 27 and added back removed code.
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
Diffstat (limited to 'backend/CMparser.mly')
-rw-r--r-- | backend/CMparser.mly | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b20dea38..5109749d 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -210,17 +210,17 @@ let mkmatch_aux expr cases = let ncases = List.length cases in let rec mktable n = function | [] -> assert false - | [_, _] -> [] - | (key, _) :: rem -> + | [key, action] -> [] + | (key, action) :: rem -> (coqint_of_camlint key, Nat.of_int n) :: mktable (n + 1) rem in let sw = Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in let rec mkblocks body n = function | [] -> assert false - | [_, action] -> + | [key, action] -> Sblock(Sseq(body, action)) - | (_, action) :: rem -> + | (key, action) :: rem -> mkblocks (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n))))) (n - 1) @@ -233,7 +233,7 @@ let mkmatch expr cases = let s = match cases with | [] -> Sskip (* ??? *) - | [_, action] -> action + | [key, action] -> action | _ -> mkmatch_aux c cases in prepend_seq !convert_accu s |