Mentions légales du service

Skip to content
  • Guillaume Melquiond's avatar
    Make theories/int.why depend on itself when generating its documentation. · 0f1c6014
    Guillaume Melquiond authored
    When theories/int.why is handled, it is missing from the environment, so
    Why3 cannot find integer operators to handle some constructs, e.g.
    variants. So this commit duplicates the file before generating the
    documentation. Luckily, links are nevertheless correct.
    
    This hack would not be needed if integer operators were builtin.
    0f1c6014