• François Bobot's avatar
    prover identification: use shortcuts · 92165a83
    François Bobot authored
       shortcuts are defined in why3.conf. They are automatically
       generated using two mechanism:
       - a shortcut section in prover-detection-data.conf creates a shortcut
       for the first prover that match the regexp
    
       - the identifier used as family argument for the prover section in
       prover-detection-data.conf is used as shortcut for the prover. If
       different sections use the same argument the first one that match an
       existing prover is used for the shortcut.
    92165a83
why3tac.ml 44.2 KB