clarify ghost and non-ghost for reals and ufloats
commit6813754dce16fba5c517be4eef9ea95552f262e0
authorMARCHE Claude <claude.marche@inria.fr>
Tue, 1 Oct 2024 13:38:42 +0000 (1 15:38 +0200)
committerMARCHE Claude <claude.marche@inria.fr>
Tue, 1 Oct 2024 13:38:42 +0000 (1 15:38 +0200)
tree5a719c7d601a8204c46ea36d13d9a56b90e4e659
parentf3d241dfee1f424b879cd2f49183f63b52c322df
clarify ghost and non-ghost for reals and ufloats
30 files changed:
examples/numeric/add_sqrt.mlw
examples/numeric/add_sqrt/why3session.xml
examples/numeric/add_sqrt/why3shapes.gz
examples/numeric/add_sub_mul.mlw
examples/numeric/add_sub_mul/why3session.xml
examples/numeric/add_sub_mul/why3shapes.gz
examples/numeric/addition.mlw
examples/numeric/addition/why3session.xml
examples/numeric/addition/why3shapes.gz
examples/numeric/exp_log.mlw
examples/numeric/exp_log/why3session.xml
examples/numeric/exp_log/why3shapes.gz
examples/numeric/lse.mlw
examples/numeric/lse/why3session.xml
examples/numeric/lse/why3shapes.gz
examples/numeric/multiplication.mlw
examples/numeric/multiplication/why3session.xml
examples/numeric/multiplication/why3shapes.gz
examples/numeric/sin_cos.mlw
examples/numeric/sin_cos/why3session.xml
examples/numeric/sin_cos/why3shapes.gz
examples/numeric/substraction.mlw
examples/numeric/substraction/why3session.xml
examples/numeric/substraction/why3shapes.gz
examples/numeric/sum.mlw
examples/regtests.sh
examples/stdlib/ufloat/why3session.xml
examples/stdlib/ufloat/why3shapes.gz
stdlib/real.mlw
stdlib/ufloat.mlw