

@2763

7 years 
sacerdot 
All daemons in compiler.ma closed (i.e. proof obligations added
to the …



@2762

7 years 
sacerdot 
All repaired up to compiler.ma.
Note: one daemon is left for one …



@2745

7 years 
sacerdot 
1. Complexity of policy computation lowered from O(n^{2) to O(n)
2. …}



@2700

7 years 
sacerdot 
1. exponential function dropped in favour of standard library
2. …



@2653

7 years 
sacerdot 
…



@2652

7 years 
sacerdot 
String type changed definition.



@2318

7 years 
boender 
 now it compiles



@2317

7 years 
boender 
 small changes to make things compile



@2316

7 years 
boender 
 committed temporary version: true version has to wait until I …



@2264

7 years 
sacerdot 
1) Major change: we now always use the efficient way of resolving …



@2230

7 years 
sacerdot 
Glue proof maximally simplified or sort of.



@2229

7 years 
sacerdot 
More cleaning up, ready for more aggressive factorization.



@2228

7 years 
sacerdot 
Further proof reduction.



@2225

7 years 
sacerdot 
Minor and major improvements everywhere, shortened proofs.



@2211

8 years 
boender 
 finished proof of sigma specification
 added some stuff to Util, as …



@2153

8 years 
boender 
 updated the proof some more



@2152

8 years 
boender 
 this should compile



@2141

8 years 
boender 
 committed working version



@2101

8 years 
boender 
 renamed medium to absolute jump
 revised proofs of policy, some …



@2078

8 years 
sacerdot 
sigma_policy_specification has been
1) strengthened
2) made nicer to …



@2059

8 years 
boender 
 updated Policy to work better



@2055

8 years 
sacerdot 
Warning: this commit adds an hypothesis that breaks all of assembly stuff.



@2034

8 years 
boender 
 split Policy into three separate files for ease (and indeed …



@2032

8 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@2018

8 years 
mulligan 
CJNE case a complete mess.



@2008

8 years 
boender 
 substantial closing of holes in proof



@1973

8 years 
boender 
 removed superfluous match
 displaced 'cases daemon'



@1965

8 years 
boender 
 further completed proof, changed jump_expansion' to reflect new type …



@1956

8 years 
boender 
 finished proof of lemma (where auto does strange things again)



@1950

8 years 
boender 
 advances in policy



@1942

8 years 
mulligan 
Work on showing the equivalence of two methods of looking up from the maps.



@1940

8 years 
boender 
 committed new version of final invariant



@1937

8 years 
boender 
 filled in some of the gaps in the proof of Policy
 reverted …



@1934

8 years 
boender 
 various & sundry moves of lemmas to better places
 integrated …



@1933

8 years 
boender 
 slight revamp



@1932

8 years 
boender 
 added some more dependent types (we love 'em)



@1931

8 years 
boender 
 added latest bvt alias
 temporary "cases daemon" commit of new …



@1886

8 years 
boender 
 improvements for disambiguation and quick(er) typing



@1879

8 years 
boender 
 Policy compiles until the end, still some (fairly trivial) cases …



@1810

8 years 
boender 
 new version of policy that compiles up to the final glue



@1809

8 years 
boender 
 committed partially compiling version of policy (up until …



@1615

8 years 
sacerdot 
Policy now depends on Assembly and not the other way around.



@1614

8 years 
boender 
 split policy from assembly
