Small factorisation: merge push & inject and pop & eject on deques
less book-keeping in proofs
cleaner proofs in Deque
Deque.deque => Deque.t
do_regularize: slightly automatize obligations proofs
cleaner extracted code, better makefile
Deque: pop & eject done.
Less ltac, less LOC overall.
Deque.inject done + mechanized proofs of obligations for push & inject
Level: added pop and eject, and the related lemmas
Level.inject done, proof automatized for push and inject in Level
update extraction mechanisme
Lots of changes, but everything is finally working
remove some uses [firstorder]
dispatch is defined
do_regularize is defined.
Types of Lvl.equilibrate and Lvl.*_cases are much preciser.
(dec_)is_empty is defined
fix: semi_regular definition was wrong
Simplified [color] definition
bugfix: [Lvl.push] definition was wrong
equilibrate is Defined
Stronger typing of [no_buffer_case]
Stronger typing of [one_buffer_case]
Stronger typing of [two_buffer_case]
Buffer.dec_is_empty is now transparent
propagate changes made to Lvl.t
minor commit: extend obligation tactic
minor commit: clean up
one_buffer_case is defined
fix: inequality notation was wrong.