Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
36 results
Created with Raphaël 2.2.023Jan222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119876543231Oct30292827262524232019181210975429Sep28272625242120191817161598628Aug26242322Improve iStartProof.MakeMorphism -> MakeEmbed.Fix error message.Make AsValid TC search not loop when there is no instance to be found.Update comment.Merge branch 'master' into gen_proofmodeFix priorities of IntoLaterN instances.Test cases for issue #141.Fix issue #141.Fix some comments.Consistently name `wp_value_inv`.Update Coq bug in comment.update .gitignoreMerge branch 'total_weakestpre'The types of propositions for monPred lemma need to be [monPred I PROP] and not [bi_car (monPredI I PROP)], otherwise iIntoValid fails in a very weird way. Seems to be related to a Coq bug.BiIndexBottom class for bottom element in a bi index. monPred_all is a monoid morphism, and related big op lemmas.Reorganize bi.monpred. Add unfolding manual lemmas for monPred_at, and use them in proofmode.monpred. Add big op lemmas for monpred_at.Merge branch 'jh/generic_updates' into 'gen_proofmode'Add instances for eliminating modalities under monPred_at or an embedding.FUpdFacts and BUpdFacts instances for monPred.Add BUpdFacts and FUpdFacts.Merge branch 'master' into gen_proofmodeAddModal: fix priorities.Merge branch 'master' into gen_proofmodeAddModal instances for except0 and later, to recover the old behaviorMerge branch 'master' into gen_proofmodeMerge branch 'robbert/add_modal' into 'master'Special proof mode class for adding a modality to a goal.Fix wrong name.Add duplicate new line at end of file.Typos.Coq 8.7.1Update examples to use total weakest preconditions.Total weakest preconditions for heap_lang.Lifting lemmas for total weakest preconditions.Prove adequacy of total weakest preconditions.Define weakest preconditions for total program correctness.Write `wp_strong_mono` in a curried way.Build `stuckness` weakening into `wp_strong_mono`.Clean up basic defs on `stuckness`.