Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.03Aug27Jul252423222130Jun29141296542131May3019141110985432130Apr292827252419181211626Mar252319201918171097543117Feb161514138432127Jan179813Dec8765430Nov29272624231817161514139231Oct2827729Sep2521206226Aug2522201716151413121110985432130Jul2726232019181615141312875428Jun272610987325May24232118171613119876CHANGELOG.Add `with_ltac1_nil`.Comment.Port `iAssert` to n-ary version.Fix bug in `iInv`.Introduce `ltac1_list_iter` and `ltac1_list_rev_iter`, make code more consistent.Add missing `_ne` prefixes.Use Ltac2 to avoid unrolling tactics notation with lists.Merge branch 'monotone-tweaks' into 'master'Merge branch 'ralf/agree_valid_included' into 'master'Comments.Improve comments, drop bogus counterexample.Counterexample for generalizing `mra A` to `A : ofe`.Rename `principal` into `to_mra` to be consistent with `agree`.Make `R` argument of `principal` implicit, it can be infered from the type of `mra R`.Tweak `mra`.Make [mra_over_rel] an opt-in moduleReplace some proofs with set_solverTheory revisionsSome proof tweaksTest problem with monotone cmraTweak proofs.Merge branch 'ralf/pair_dist' into 'master'add pair_distadd agree_valid_includedadd more option-included lemmasMerge branch 'ralf/singleton_included_mono' into 'master'Merge branch 'fupd_plain_soundness_no_lc_strong' into 'master'Add fupd_plain_soundness_no_lc_strongMerge branch 'robbert/bi_persistently_mixin' into 'master'Improve comment.rename `singleton_mono` to `singleton_included_mono`CHANGELOG.Comments.Add heapprop_affine.Show that for non-step indexed BIs, <pers> can trivially be inhabited.Merge branch 'ike/internal_included' into 'master'CHANGELOG.More tweaks, add comment on hintsTweak proofs.