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.013Jul976543230Jun29282625232221201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221201918161514131298763231Jan29272524Merge branch 'gen_proofmode' into 'master'Fix CHANGELOG.md markdownexpand changelogREADME: add link to MoSeL paper websiteCoq master is fixedCHANGELOGdisable building against coq.dev as upstream is currently brokenMore consistent names for modality actions.heap_lang/proofmode: move pm_prettify to where we used to do lazy betaMerge branch 'ralf/pm' into 'gen_proofmode'update iApply prettification testcase to use something that actually still prettifiesuse iDestructHyp instead of iDestructMerge branch 'ralf/wp_alloc' into 'gen_proofmode'wp_alloc: test more patternsrename Declare Reduction to match the tacticsadd lemma names to proofmode.refSplit prettification from proof mode reductionremove big_opL from prettification listmake `wp_alloc l as "?"` behave as expectedchangelogMerge branch 'ci/ralf/telescopes' into 'gen_proofmode'Move laterN_iter to derived_laws_sbi, because it's more generic.make sbi_laterN compute and rely on that instead of MakeLaterNadd some more printing to some testsconsistently use pm_prettify for post-tactic simplificationproofmode: normalize big_opLtest and fix more telescope normalizationfix nitsadd general telescopes and telescopic BI binders and proofmode supportmake pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbnMerge branch 'ralf/cas' into 'gen_proofmode'add wp_cas tactic that performs case distinction; weaken logatm heap to be easier to usemake README ready for mergerCHANGELOGAllow comparing even more values in CAS by making things more consistentwe can allow comparing more things -- and explain whyMerge branch 'master' into gen_proofmodebump std++Bump std++.More Implicit Types.