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.018Jan16131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119876543231Oct302928272625242019181210975429Sep282726252421201918171598628Aug26242322201776428Jul14121027Jun13128Reorganize 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`.Bump stdpp.Mention Coq issue 6583.Fix bug reference.Use [notypeclasses refine] instead of eapply in iLöb and iNext, to workaround the confusion of apply wrt canonical structures.FromAssumption instances.Minimal proof mode support for monPred_exIntroduce monPred_ex, add monPred_in rules (attemp at removing abstract views from iGPS.Better follow naming convention: biIndex.Renaming monPred_car -> monPred_atAdd comment about lazy TC to `iPoseProofCore`.Add 0d6031e4 to the changelog.Fix issue #128.Make `wp_expr_eval` a `Tactic Notation` so that the argument is parsed as a tactic.`iSimpl` tactic that `simpl`s the proofmode goal.Rename `timelessP` into `timelessP`.Merge branch 'janno/monfun' into 'gen_proofmode'