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.04Mar32128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov2928272624232221201816151413121198765432Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmodeSplit [FromAssumption] into three, depending on wheter the parameters are evars. This is to avoid loops in TC search.Merge branch 'robbert/big_rename' into 'gen_proofmode'Typo.Notations <absorb>, <affine> and <pers>.Notations <obj> and <subj>.Rename absolutely → objectively and relatively → subjectively.We usually fail faster to prove IntoPure than Absorbing/Affine.More Hint Modes.Add iStartProof in iAccu.Add classes BiEmbedFUpd and BiEmbedBUpd for the interractions between embeddings and updates.Error message for iAccu.Fix build by being a little bit less restrictive in Hint Modes.Fix build.Fix Hint Modes and add some.Get rid of KnownFrame and iFrame automatically instantiating evars.Add iAccu tactic.Merge branch 'robbert/bundle_bi_classes' into 'gen_proofmode'Some comments.A type class for plainly.Bundle type class for embedding.Bundle update type class.Merge branch 'robbert/FromLaterN_be_gone' into 'gen_proofmode'Get rid of `FromLaterN` class.Merge branch 'jh/evar_iframe' into 'gen_proofmode'Prefer modality over embedding in `iModIntro`.Make iFrame able to accumulate assertions in an evar.Break a depedency.Turn some MaybeLaterN instances into LaterN instances.Replace elim_inv_embed_inv by the more generic instance elim_inv_embed.Support to specify the modality to introduce in `iModIntro`.Improve comment.Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmodeAdd instance elim_inv_embed_inv.Remove duplicate modality instances.Less hacky fix than d1b836c8.Make sure iNext works even if the entailment is not directly an sbi entailment.Merge branch 'robbert/super_iModIntro' into 'gen_proofmode'Update ProofMode.md w.r.t. the changes to `iModIntro`.Define `MaybeIntoLaterNEnvs` in terms of the new classes.