• Sylvain Dailler's avatar
    Adding a test file. · 3cd2c274
    Sylvain Dailler authored
    Struggling with names. Removed the print_task which looked at the driver
    before printing for uniformity. If I dont do that the printing function
    I use to have a safe naming environnment inside tasks are not the same
    as the printing function we use for display. So hypothesis displayed dont
    actually exists and other bugs.
    I will try to see if my changes (in particular clean_environnment and
    gen_ident) are necessary.
    Modifications in Pretty to get real unique names for hypothesis.
why3shell.ml 18.1 KB