MARCHE Claude 89a894b47a do not map IEEE floats theory to Alt-Ergo's own theory ...

Upgrade to AE 2.6.2

2025-06-18 10:45:29 +09:00

..

mach

Remove some trailing spaces.

2024-12-07 09:01:55 +01:00

algebra.mlw

add a meta to mark a symbol as never removed by remove_unused*

2023-06-15 15:18:48 +00:00

array.mlw

Separate logical and program function Array.make

2021-01-15 12:39:37 +01:00

bag.mlw

Mark some types as having an extensional equality.

2024-11-13 19:04:52 +01:00

bintree.mlw

coma_vc: minor fix

2024-08-08 09:06:07 +02:00

bool.mlw

Pmodule: t->t->t functions can be overloaded as X->X->t functions

2024-09-19 10:54:24 +02:00

bv.mlw

Merge remote-tracking branch 'why3-inria/master' into why3-devel

2024-12-13 17:34:11 +01:00

byte_string.mlw

stdlib: proper postcondition for (=) on bounded integers

2023-06-17 00:16:27 +00:00

coma.coma

coma: update stdlib + examples

2024-08-08 11:09:46 +02:00

cursor.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

debug.mlw

…

exn.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

floating_point.mlw

Generalization of check_unused_vars to logic and program decl

2019-08-20 15:48:44 +02:00

fmap.mlw

Mark some types as having an extensional equality.

2024-11-13 19:04:52 +01:00

for_drivers.mlw

Revert "Simplify euclidean to computer division"

2023-10-19 12:12:59 +02:00

function.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

graph.mlw

stdlib, examples: remove redundant "import"

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

hashtbl.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

ieee_float.mlw

Merge remote-tracking branch 'why3-inria/master' into why3-devel

2024-12-13 17:34:11 +01:00

int.mlw

do not map IEEE floats theory to Alt-Ergo's own theory

2025-06-18 10:45:29 +09:00

io.mlw

Document module "io" (fix #554).

2021-09-23 15:11:55 +02:00

list.mlw

stdlib list.mlw: Add contract to Quant.{for_all, for_some, mem}

2019-10-01 15:23:25 +02:00

map.mlw

Mark some types as having an extensional equality.

2024-11-13 19:04:52 +01:00

matrix.mlw

Matrix: add the pure "update" function for applicative updates

2018-07-02 17:15:42 +02:00

microc.mlw

Dexpr: emit a warning for spurious olds in val contracts

2021-03-12 20:56:41 +01:00

number.mlw

stdlib, examples: remove redundant "import"

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

ocaml.mlw

stdlib: ocaml exception Invalid_argument moved to ocaml.Exceptions

2020-06-22 18:38:26 +02:00

option.mlw

stdlib: added a new theory option.Map

2020-08-25 14:53:07 +02:00

pigeon.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

pqueue.mlw

Add safe_peek and safe_pop in all pqueue modules

2019-07-03 16:11:41 +02:00

python.mlw

micro-Python: add_list can be used in logic

2022-11-14 14:58:24 +01:00

queue.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

random.mlw

stdlib, examples: remove redundant "import"

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

real.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

ref.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

regexp.mlw

stdlib: update Regexp to use sequences

2024-03-20 18:13:00 +01:00

relations.mlw

Changed the unsecure trusted_wf attribute mechanism into a more secure one

2023-02-22 13:50:29 +00:00

seq.mlw

fix realizations

2024-11-13 19:10:42 +01:00

set.mlw

fix realizations

2024-11-13 19:10:42 +01:00

stack.mlw

library: {Stack,Queue}.length now return a Peano.t

2018-10-26 15:47:03 +02:00

string.mlw

Mark some types as having an extensional equality.

2024-11-13 19:04:52 +01:00

tptp.mlw

stdlib, examples: remove redundant "import"

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

tree.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

ufloat.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

witness.mlw

library: two versions of witness

2018-06-17 11:09:22 +02:00