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.01Apr31Mar272523212019181613121096428Feb2625242320191817151413121110765432130Jan292321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312987630Jul221413129753130Jun2928272625242120191817161514131211109765Merge branch 'robbert/iso' into 'master'Some Coqdoc improvements in the OFE file.CHANGELOG.Make use of OFE isomorphisms in COFE solver.Add notion of isomorphism between OFEs.these are all functors from OFEsmention which categories these functors map to whichMerge branch 'inj-typeclass-2' into 'master'Revise uses of `inj` from !408 as discussedProve that `≡` is limit preserving.Let `iNext` detect equalities `Next x ≡ Next y`.Merge branch 'inj-typeclass' into 'master'Replace explicit use of Inj instances by injMerge branch 'msammler/fix_drop_insert' into 'master'drop_insert -> drop_insert_gtMerge branch 'add-missing-proof' into 'master'Add missing `Proof.` to sealing proofsMerge branch 'spell-check' into 'master'Spell check proof_guide.mdMerge branch 'sbi-eq-notation-sections' into 'master'sbi_internal_eq: add "sections" of notation, following stdppMerge branch 'robbert/atomic_wp_seq_step' into 'master'Prove stepping (i.e., non-value) version of `atomic_wp_seq`.Merge branch 'robbert/exist_laterable' into 'master'Prove `Laterable (∃ x, Φ x)`.Remove redundant space.Merge branch 'vscode-editor-docs' into 'master'Add VS code to the editor.md docsMerge branch 'robbert/iAssumption' into 'master'Add documentation.CHANGELOG entry.Make `iAssumption` work on `⊢ ...` premises in the Coq context.Fix errors of `iAssumption`, `iExact`, and friends.Fix bad line break.Instance for `Affine (□?p P)`.update dependenciesFix Coqdoc.Merge branch 'ci/ralf/pair_core_id' into 'master'Avoid slow `try done`.change some other hints to a more general pattern and typeclass instances