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.014Feb131298763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119876543231Oct302928272625242019181210975429Sep28272625Remove Admitted.Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodeavoid type ascriptionAdd test for #146.consistent non-parentheses for Implicit Typesexplain why we use typeclasses eautoset modes for update modality typeclassessolve AsValid without solving all the other evars firstStep being verbose when the CI preparation script is donemore parallel CIupdate CI; time Coq 8.7.1Fix build by using envs_entails everywhere and by not breaking this abstraction in tactics.Opaque is not enough. Let's seal envs_entails.Make envs_entails opaque.Fix doc.Wrong kind of comment.Merge branch 'jh/affine_frompure' into 'gen_proofmode'More doc about FromPure.Merge branch 'robbert/issue_154' into 'gen_proofmode'Make FromPure depend on an affinity parameter.Revert "Make FromPure depend on an affinity parameter."Make FromPure depend on an affinity parameter.document the RA model brieflyRestore side-condition of `iMod` tactic and `ElimModal` TC.Remove hacks that are no longer needed.Makefile: honor COQBINBump stdpp.Merge branch 'ci/robbert/no_backtracking' into 'master'Fix issue #153 by using `NoBackTrack` in the `Frame` instances for ▷.Bump stdpp.Document BI axioms in terms of the axioms in the ordered RA model.Note that `plainly` will be removed from the BI interface.Merge branch 'robbert/iFrame_improvements' into 'master'Bump stdpp and fix the CI (hopefully).Merge branch 'robbert/super_iAlways' into 'gen_proofmode'Tests for framing under conjunctions.Frame in both sides of a conjunction.Support framing under implications.Some test cases/uses for stronger framing in disjunctions.Better framing support for disjunctions.