MARCHE Claude 715fa89d16 separate transformations for intros, dequant, and remove_unused ...

remove unused before reflection transformation

avoid subst to a unused symbol

2023-04-25 12:20:08 +00:00

..

compiler

fix sessions

2022-07-07 15:49:23 +02:00

imp

update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible

2023-04-05 13:48:22 +02:00

logic

update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible

2023-04-05 13:48:22 +02:00

specs

separate transformations for intros, dequant, and remove_unused

2023-04-25 12:20:08 +00:00

state

Add a initial comment in shapes files

2021-08-25 10:49:04 +00:00

vm

update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible

2023-04-05 13:48:22 +02:00

compiler.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

imp.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

logic.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

specs.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

state.why

example double-wp: use strong invariant instead of correctness predicates

2017-06-07 18:13:39 +02:00

vm.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00