- 12 Feb, 2014 5 commits
-
-
MARCHE Claude authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
If the record update { expr with f1 = ...; f2 = ... } updates each field in the record, the intermediate variable for expr is unused. Avoid the warning by naming this variable "_q ".
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 11 Feb, 2014 6 commits
-
-
MARCHE Claude authored
-
Andrei Paskevich authored
It should be noted that 2ff8efca disables the "forgotten diverges" warning for Eabstr, which changes the behaviour, but is a good idea anyway.
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
as follows: maps: permut_sub -> permut arrays: map_permut_sub -> permut (to be consistent with maps) permut_sub -> permut_sub permut -> permut_all
-
Martin Clochard authored
-
- 10 Feb, 2014 4 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Martin Clochard authored
-
Martin Clochard authored
-
- 08 Feb, 2014 3 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 07 Feb, 2014 5 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
Ca m'apprendra a commiter/pusher trop vite...
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 06 Feb, 2014 4 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
grants a long-standing feature wish by Andrei
-
Jean-Christophe Filliâtre authored
this is a contribution of Laurent Théry
-
Jean-Christophe Filliâtre authored
-
- 05 Feb, 2014 4 commits
-
-
Jean-Christophe Filliâtre authored
predicates permut over maps and arrays are given new semantics, as follows: - MapPermut: permut m1 m2 l u means that m1[l..u[ is a permutation of m2[l..u[ and values outside the interval [l..u[ are *ignored*. - ArrayPermut: permut_sub a1 a2 l u means that a1[l..u[ is a permutation of a2[l..u[ and other meaningful values are *identical*. - ArrayPermut: another predicate map_permut_sub has the same semantics as MapPermut.permut_sub, that is values outside of the interval [l..u[ are ignored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 04 Feb, 2014 2 commits
-
-
François Bobot authored
-
Jean-Christophe Filliâtre authored
-
- 03 Feb, 2014 7 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-