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

Upgrade to AE 2.6.2

2025-05-22 19:49:00 +02:00

..

mach

Do not introduce program variables for zero and one in int.Int module

2025-03-26 15:17:05 +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

fix realizations

2024-11-13 19:10:42 +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

reflection printfs and add_limbs example

2018-01-16 11:15:11 +01:00

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

Merge remote-tracking branch 'origin/master' into computer_division_for_master

2018-06-21 23:01:11 +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

Adding a function from_real in the theory of IEEE floats

2024-11-03 21:13:10 +01:00

int.mlw

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

2025-05-22 19:49:00 +02:00

io.mlw

Document module "io" (fix #554).

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

list.mlw

list.Distinct using a recursive definition

2025-05-14 17:32:28 +02:00

map.mlw

map.MapPermut is a permutation

2025-05-07 23:43:38 +02: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

map.MapPermut is a permutation

2025-05-07 23:43:38 +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

SLSE full proof

2025-03-10 16:00:09 +01: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

add simple examples of iterators on sets with extraction to OCaml

2025-03-26 17:20:01 +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

SLSE full proof

2025-03-10 16:00:09 +01:00

witness.mlw

library: two versions of witness

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