repo.or.cz
/
why3.git
/
search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
log
|
graphiclog1
|
graphiclog2
|
commit
|
commitdiff
|
tree
|
refs
|
edit
|
fork
first
·
prev
·
next
Merge branch 'letify_generated_formula' into 'master'
2024-05-07
Jean-Chr
i
s
to
p
he
.
.
.
Merge
b
ran
c
h
'improve-error-message-on-
u
n
k
n
own-
m
odule
.
.
.
commit
|
commitdiff
|
tree
2024-05-07
J
e
an-C
h
ris
t
ophe
.
.
.
M
erge
bra
n
c
h
'e
x
traction-cre
a
te-prefix-paths-of-files
.
.
.
commit
|
commitdiff
|
tree
2024-05-05
Jean-Christophe
.
.
.
Merge bra
n
ch 'long
e
st-increasing-subsequence' into
.
.
.
commit
|
commitdiff
|
tree
2024-05-05
Jean-C
h
ristophe
.
.
.
new exampl
e
: longe
s
t increasing subse
q
uence
commit
|
commitdiff
|
tree
2024-05-02
Jean-Christophe
.
.
.
Merge branch 'p
r
oper_cuts'
i
nto 'mast
e
r'
commit
|
commitdiff
|
tree
2024-05-02
Jean-
C
hristophe
.
.
.
new e
x
a
m
ple: proper cu
t
s
commit
|
commitdiff
|
tree
2024-04-13
Jean-Christophe
.
.
.
M
e
rge b
r
anch 'bet
t
er_na
m
es_in_eval_match' into 'master'
commit
|
commitdiff
|
tree
2024-04-10
Jean-C
h
ristophe
.
.
.
M
erge
b
r
anch 'toy-c
o
mpiler-cleani
n
g-and-documentation
.
.
.
commit
|
commitdiff
|
tree
2024-04-10
J
e
an-Christophe
.
.
.
toy compiler example:
c
leaning and docume
n
tatio
n
commit
|
commitdiff
|
tree
2024-04-05
Jean-Christ
o
ph
e
.
.
.
Merge
b
ranch 'anagrammi' into '
m
as
t
er'
commit
|
commitdiff
|
tree
2024-04-05
Jean-Christophe
.
.
.
Merge branc
h
'anagrammi' int
o
'master'
commit
|
commitdiff
|
tree
2024-03-20
Jean-Chr
i
sto
p
he
.
.
.
Me
r
g
e
branch 'rege
x
p_seq
'
i
nto
'm
a
ster'
commit
|
commitdiff
|
tree
2024-03-20
Jean-Christop
h
e
.
.
.
Merge branch '
t
wo-files-to-b
e
-
ignored' into 'master'
commit
|
commitdiff
|
tree
2024-02-11
J
ea
n
-Christoph
e
.
.
.
Me
r
ge br
a
n
ch 'new-ex
a
mple
-
ka
d
a
ne-variant
'
into
'
master'
commit
|
commitdiff
|
tree
2024-02-03
Jean-Christophe
.
.
.
M
e
rge branch 'new-
e
xample-array-of
-
lis
t
'
into 'master'
commit
|
commitdiff
|
tree
2024-01-31
J
e
an-Christophe
.
.
.
Merge
branch 'im
p
roved-mex-ex
a
mple' int
o
'master'
commit
|
commitdiff
|
tree
2024-01-27
Je
a
n-Chris
t
ophe
.
.
.
Merge
b
ranch 'remove-unsound-modu
l
e
-Null' into
'ma
s
ter'
commit
|
commitdiff
|
tree
2024-01-24
Jean-Christophe
.
.
.
Mer
g
e branch 'split-string-e
x
ample'
i
n
to
'
m
a
ster'
commit
|
commitdiff
|
tree
2023-10-16
Jean-Christophe
.
.
.
Merge
branch 'just_join' into 'master'
commit
|
commitdiff
|
tree
2023-08-25
J
ean-Christop
h
e
.
.
.
Mer
g
e branch 'add-
d
u
mmy-prelude-printe
r
' into
'
master'
commit
|
commitdiff
|
tree
2023-07-26
Jean-
C
hristophe
.
.
.
M
e
r
g
e branch 'improv
e
d-power-e
x
ample' into 'master'
commit
|
commitdiff
|
tree
2023-05-09
Jea
n
-Christophe
.
.
.
Merge
b
r
anch 'sp
a
ce_saving
_
algorithm' into 'master'
commit
|
commitdiff
|
tree
2023-04-19
Jean-Chris
t
ophe
.
.
.
Merge
b
ranch 'flexib
l
e_ar
r
ays' into 'master'
commit
|
commitdiff
|
tree
2023-04-08
J
ean-
C
hr
i
s
t
oph
e
.
.
.
Merge branc
h
'74
8
-confusin
g
-
t
ype
-
error
-
messa
g
e' into
.
.
.
commit
|
commitdiff
|
tree
2023-04-07
J
e
a
n
-Christophe
.
.
.
Merge branch 'imp
r
ov
e
d-balance-puzzle-
a
gain' into
.
.
.
commit
|
commitdiff
|
tree
2023-04-04
J
ean-Christophe
.
.
.
Merge branch 'improved-balance-
p
uzzle' i
n
to 'mast
e
r'
commit
|
commitdiff
|
tree
2023-02-17
Jean-Christophe
.
.
.
M
e
rge br
a
nch '
b
inomial_co
e
fficient' into 'master'
commit
|
commitdiff
|
tree
2022-11-14
Jean-Christophe
.
.
.
Merge branch 'micro-python-stdl
i
b' into 'master'
commit
|
commitdiff
|
tree
2022-11-14
Jean-
C
hrist
o
phe
.
.
.
Merge branc
h
'
m
icro-python-
b
y-so' into 'master'
commit
|
commitdiff
|
tree
2022-11-06
Jea
n
-Christophe
.
.
.
M
erge br
a
nch 'yet-yet-anothe
r
-list-reversal' into
.
.
.
commit
|
commitdiff
|
tree
2022-10-24
Je
a
n-C
h
r
ist
o
phe
.
.
.
Merge bra
n
ch
'yet-yet-another-list-re
v
e
rs
a
l' i
n
to
.
.
.
commit
|
commitdiff
|
tree
2022-09-09
Jean-Ch
r
istophe
.
.
.
Merge
branc
h
'yet-another-list-r
e
versal
'
i
nto 'mas
t
er'
commit
|
commitdiff
|
tree
2022-09-08
Jean-Chris
t
ophe
.
.
.
Mer
g
e branch
'improved-python-plug
i
n' into 'master'
commit
|
commitdiff
|
tree
2022-09-08
J
e
a
n
-Christ
o
p
he
.
.
.
Python
:
do
c
ument
a
ti
o
n
commit
|
commitdiff
|
tree
2022-09-08
Jean-Christophe
.
.
.
P
y
tho
n
:
doc
u
menta
t
ion
commit
|
commitdiff
|
tree
2022-08-26
Je
a
n-Christoph
e
.
.
.
Merge branch 'yet_another_s
o
rtin
g
_algorithm' into
.
.
.
commit
|
commitdiff
|
tree
2022-08-26
Jean-Christophe
.
.
.
Merge b
r
an
c
h
'new-version-of-tu
r
in
g
-factorial' into
.
.
.
commit
|
commitdiff
|
tree
2022-05-04
Jean-Christophe
.
.
.
Merg
e
branch 'lemm
a
s-as-lemma-funct
i
on
s
' into 'master'
commit
|
commitdiff
|
tree
2022-04-25
J
e
a
n
-Christophe
.
.
.
M
erge b
r
a
nch 'auto-detecti
o
n' into 'mas
t
e
r'
commit
|
commitdiff
|
tree
2021-12-09
Jean-Chri
s
t
o
phe
.
.
.
Merge branch
'fixed-python
-
lexer' into '
m
aster'
commit
|
commitdiff
|
tree
2021-10-29
Jean-Christophe
.
.
.
M
e
r
g
e branch
'
fix-configure-detecti
o
n-cam
l
z
i
p
'
i
nto
.
.
.
commit
|
commitdiff
|
tree
2021-10-29
Jea
n
-
C
hr
i
st
o
phe
.
.
.
M
e
r
ge branch 'micro-python-pow' into 'master'
commit
|
commitdiff
|
tree
2021-09-30
Jea
n
-Christophe
.
.
.
Merge branch 'micro-python-
l
ogic-def-and-type-variabl
e
s
.
.
.
commit
|
commitdiff
|
tree
2021-09-28
Jean-Christophe
.
.
.
Merge branc
h
'micro-p
y
thon-types-in-quantifiers' in
t
o
.
.
.
commit
|
commitdiff
|
tree
2021-09-24
Jean-Chri
s
tophe
.
.
.
Merge branch 'typ
e
s
-
in-micro-pyth
o
n' int
o
'
master'
commit
|
commitdiff
|
tree
2021-07-08
Jean-Christophe
.
.
.
M
erge branch
'
internship-2021-LMF' into 'mast
e
r'
commit
|
commitdiff
|
tree
2021-06-11
Je
a
n-Chris
t
ophe
.
.
.
Merge
b
ra
n
c
h 'i
n
f
i
nity_of_primes
'
into 'm
a
ste
r
'
commit
|
commitdiff
|
tree
2021-03-30
Jean-C
h
risto
p
he
.
.
.
Merge branch 've
r
ify
t
h
i
s_2021_soluti
o
ns' into '
m
ast
e
r
'
commit
|
commitdiff
|
tree
2021-03-30
Jean-Christo
p
he
.
.
.
Merge branch 'verifythis_
2
021_solut
i
ons' into 'maste
r
'
commit
|
commitdiff
|
tree
2021-03-27
Je
a
n-
C
hristophe
.
.
.
Merge
branch 'wrap_lines
'
into '
m
aster'
commit
|
commitdiff
|
tree
2021-03-08
Jean-
C
hristoph
e
.
.
.
M
erge branch 'hoare-eu
c
l-div' in
t
o 'mast
e
r'
commit
|
commitdiff
|
tree
2021-01-07
Jean-Ch
r
i
s
t
o
phe
.
.
.
Merge branch
'524-why3-pr
o
v
e-raise
s
-
n
ot_
f
ound-when
.
.
.
commit
|
commitdiff
|
tree
2020-12-11
Jean
-
C
h
r
istophe
.
.
.
Merge branch
'a
l
lows-namespace-in-for-each'
in
t
o 'master'
commit
|
commitdiff
|
tree
2020-02-28
Jean-Chr
i
s
tophe
.
.
.
Merge branch 'for_
e
ach' into
'
master'
commit
|
commitdiff
|
tree
2020-02-11
Jean-Ch
r
ist
o
phe
.
.
.
Apply suggestion to
t
e
s
ts/tes
t
_foreach
.
mlw
commit
|
commitdiff
|
tree
2019-06-06
Jean-Christ
o
phe
.
.
.
Merge br
a
nch
'
q
ue
u
e' into 'master'
commit
|
commitdiff
|
tree
2010-11-05
Jean-Chr
i
stophe
.
.
.
make foo
.
gui instea
d
of
make
foo to call why
i
de
commit
|
commitdiff
|
tree
2010-11-04
Jean-Christophe
.
.
.
next_digit_sum
:
safet
y
done
;
correct sum done
commit
|
commitdiff
|
tree
2010-11-04
Jea
n
-Christophe
.
.
.
(no commit me
s
s
a
ge)
commit
|
commitdiff
|
tree
2010-10-28
Jean-C
h
rist
o
phe
.
.
.
vaci
d
-0
commit
|
commitdiff
|
tree
2010-10-28
Je
a
n
-
C
hristophe
.
.
.
vaci
d
-0:
red bl
a
ck tree
s
in progress
commit
|
commitdiff
|
tree
2010-10-28
J
ean-
C
h
ristophe
.
.
.
v
ac
i
d
-
0:
r
e
d bla
c
k tr
e
es in
pr
o
gr
e
ss
commit
|
commitdiff
|
tree
2010-10-28
Je
a
n-Christophe
.
.
.
vacid-0:
red black
trees
(
harness don
e
)
commit
|
commitdiff
|
tree
2010-10-26
Jean-Christophe
.
.
.
the tes
t
s for
t
he
'
for'
loop are include
d
in
t
he set
.
.
.
commit
|
commitdiff
|
tree
2010-10-26
Je
a
n-Christop
h
e
.
.
.
p
r
ograms: the 'do
w
nto
'
variant of the for l
o
op
commit
|
commitdiff
|
tree
2010-10-26
Jean-
C
hri
s
t
o
phe
.
.
.
pr
o
grams
:
as a
s
i
d
e-effect
o
f the new for loop, the
.
.
.
commit
|
commitdiff
|
tree
2010-10-26
Jean-Ch
r
i
s
t
ophe
.
.
.
programs:
added a for lo
o
p
,
w
ith Ocaml
seman
t
i
c
s and
.
.
.
commit
|
commitdiff
|
tree
2010-10-26
Jean-
C
hris
t
ophe
.
.
.
e
x
amples : next_
d
i
g
it_sum still in p
r
ogress
commit
|
commitdiff
|
tree
2010-10-26
Jean-Christoph
e
.
.
.
alt-ergo driver: fi
x
ed inc
o
rrect syn
t
ax %%
into
%
commit
|
commitdiff
|
tree
2010-10-25
Jean-Christo
p
he
.
.
.
programs:
nex
t
e
x
am
p
le in
ne
x
t_digit
_
s
u
m (work i
n
progress
.
.
.
commit
|
commitdiff
|
tree
2010-10-25
Je
a
n-Chr
i
s
tophe
.
.
.
program
s
: fixed typing rela
t
ed to exceptions which
.
.
.
commit
|
commitdiff
|
tree
2010-10-25
J
ean-Ch
r
i
s
tophe
.
.
.
(
n
o
c
ommit
m
essage)
commit
|
commitdiff
|
tree
2010-10-25
Jea
n
-Christo
p
he
.
.
.
(
no
commit mess
a
g
e)
commit
|
commitdiff
|
tree
2010-10-22
J
e
an-Christophe
.
.
.
v
acid0/sparse array: added VC for ar
r
a
y
ac
c
ess wit
h
in
.
.
.
commit
|
commitdiff
|
tree
2010-10-13
Jean-Ch
r
istoph
e
.
.
.
Coq output: fixed s
y
ntax for algebraic data
t
ypes declaratio
.
.
.
commit
|
commitdiff
|
tree
2010-10-12
Je
a
n-Christo
p
h
e
.
.
.
e
xa
m
ples: vacid0 union-find
:
build_maz
e
cons
i
sten
t
.
.
.
commit
|
commitdiff
|
tree
2010-10-12
Jean
-
Christo
p
he
.
.
.
f
i
xed -1
offset in program
'
s annotation lo
c
a
tions;
.
.
.
commit
|
commitdiff
|
tree
2010-10-07
Jean-Christophe
.
.
.
programs: fixe
d
bug in
WP for try/with
commit
|
commitdiff
|
tree
2010-09-24
J
e
an-Christophe
.
.
.
p
r
ogram
s
/
e
x
a
mples/d
i
jkstra: implem
e
nt
a
t
i
on
o
f relax
commit
|
commitdiff
|
tree
2010-09-24
Jean-Chr
i
stophe
.
.
.
p
r
ograms/examples/dijkst
r
a: impleme
n
t
a
tion of rela
x
.
.
.
commit
|
commitdiff
|
tree
2010-09-23
Jean-Christophe
.
.
.
programs: m
o
re terms and form
u
las are
l
abell
e
d
commit
|
commitdiff
|
tree
2010-09-23
Jean-Christophe
.
.
.
progra
m
s
:
more ter
m
s and
f
ormulas are labelled
commit
|
commitdiff
|
tree
2010-09-23
Jean-Christophe
.
.
.
- Den
v
.
specializ
e
keeps labels
commit
|
commitdiff
|
tree
2010-09-20
J
e
an-C
h
ristophe
.
.
.
program
s
: no
more a
r
row
t
y
p
es in the l
o
gical
e
nvironment
commit
|
commitdiff
|
tree
2010-09-15
Jean-Chris
t
ophe
.
.
.
v
ersion of
E
pro
v
e
r
commit
|
commitdiff
|
tree
2010-08-23
Jea
n
-Chr
i
s
t
op
h
e
.
.
.
p
r
ograms: benc
h
files for
p
olymo
r
p
h
ic references
commit
|
commitdiff
|
tree
2010-08-20
Jean-Christophe
.
.
.
programs: fixed typing of
p
oly
m
orphi
c
r
eferences
commit
|
commitdiff
|
tree
2010-08-18
Jean-C
h
ri
s
tophe
.
.
.
p
rograms
:
fixed capture bug in program
t
ypes
commit
|
commitdiff
|
tree
2010-08-18
J
e
a
n
-Christophe
.
.
.
programs: less constr
u
cts in ab
s
tract
syntax
commit
|
commitdiff
|
tree
2010-08-18
Jean-Christophe
.
.
.
= replaced by ls
_
equal in core/
p
retty (was discove
r
ed
.
.
.
commit
|
commitdiff
|
tree
2010-08-16
Jean
-
Christophe
.
.
.
ignore
u
p to date
commit
|
commitdiff
|
tree
2010-08-16
Jean-Chris
t
ophe
.
.
.
progra
m
s:
fixed the freshness test (
o
nly references
.
.
.
commit
|
commitdiff
|
tree
2010-08-12
Jean-Chris
t
o
p
he
.
.
.
programs: added freshness analysis for references r
e
tur
n
e
d
.
.
.
commit
|
commitdiff
|
tree
2010-08-12
Jean-Ch
r
istophe
.
.
.
programs
:
typ
i
ng
n
ow rejects aliases
commit
|
commitdiff
|
tree
2010-07-21
Jea
n
-
Christophe
.
.
.
t
h
e
ories: mo
n
omo
r
phic
v
ersions o
f
arrays
commit
|
commitdiff
|
tree
2010-07-21
J
e
an
-
Chris
t
ophe
.
.
.
t
h
eories
:
no more string (use array
.
ArrayMonoR
i
c
h instead
.
.
.
commit
|
commitdiff
|
tree
2010-07-20
J
e
a
n-Christo
p
he
.
.
.
programs: no quantif
i
cation over
v
a
r
iables of type
.
.
.
commit
|
commitdiff
|
tree
2010-07-19
Je
a
n-Christophe
.
.
.
coq-plugin fi
x
ed
(t_case
a
nd
f
_case
c
hanges)
commit
|
commitdiff
|
tree
2010-07-16
J
ean-Christophe
.
.
.
programs:
r
o
pes
commit
|
commitdiff
|
tree
2010-07-16
Jean-Ch
r
istophe
.
.
.
programs:
type-checking the
a
ny construct
commit
|
commitdiff
|
tree
next