1. Peter_Sewell
  2. lem
Issue #33 resolved

Indentation in Coq generated code

Robin Morisset
created an issue

Some line returns are missing in pattern matches. It is especially visible in the file MachineDefInstructionSemantics.v (generated from the Lem operational formalisation of the Power model), where there are imbricated matches in ppc_sem_of_instruction. It currently looks like this:

match (i) with |... => ...
  | ... => match
    ...
    end | ... => ...

while this would look much more readable:

match (i) with
  | ... => ...
  | ... => match
    ...
    end
  | ... => ...