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.04Aug327Jul252423222130Jun29141296542131May3019141110985432130Apr292827252419181211626Mar252319201918171097543117Feb161514138432127Jan179813Dec8765430Nov29272624231817161514139231Oct2827729Sep2521206226Aug2522201716151413121110985432130Jul2726232019181615141312875428Jun272610987325May24232118171613fix testadd a test documenting recently changed behaviorupdate dependenciesMerge branch 'robbert/iInduction_regression_931' into 'master'Merge branch 'ralf/i-start-proof-hack' into 'master'Fix `iInduction` regression caused by !931.hack: temporarily revert 'iIntros (x)' doing iStartProofiStartProof: print what is not a BI assertionFix bug in iLöb caused by n-ary intros change.Merge branch 'robbert/setoid_docs' into 'master'Tweaks.Improvements by Ralf.Some documentation about `Params` and `Proper`.Merge branch 'ralf/some-included-refl' into 'master'Merge branch 'janno/ltac2-ltac1-lists' into 'master'renameCHANGELOG improvements by Ralf.Address review feedback.Use `_` prefix for private/internal tactics.CHANGELOG.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 cmra