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.026Dec232221201918161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug302928272625242322212019181716Ofe and Cofe structures on vectors.Version of [fixpoint_ind] that is easier to use.Coinduction principle on fixpoints.New derived lemma : entails_equiv_and.Slices are contractive.Tweak core.vcore: fix typo in lemma namefewer linebreaks in the coreImplement JH's idea of a "core of an assertion"fix buildmove gen_heap to base_logic. It does not depend on WP or antyhing language-specific.ssreflect 1.6.1 is out :)uPred entailment commutes over limitsFix issue #54.show na_own_accfix an error message in iInductionshow lemma about big_sepL and zip_withadd decide_left, decide_rightCI: script spacingfix coq 8.6 CI job namebuild against the released Coq 8.6make ndisj hints look through definitions to unfold more stuffMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqfix assigning priority to ndisj hintMove stuff out of sections that does not depend on the section variables.Simplify proofs relating nth to lookup.proofmode: show that quantifiers preserve puritylist: relate nth and lookupdo make validate with just 10% probabilityfix CIre-enable make validate on CIagree: prove non-step-indexed uninjectionUse different module structuring of uPred.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqturns out naming the module dec_agree_deprecated is not necessaryTry to speed up framing with fractional.A few lemmas about vec and fin.Some tweaks.Merge heap_lang/wp_tactics.v into heap_lang/proofmode.v.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq