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.027Sep2120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May302928272524232221201913121110976432Extend iClear to handle clearing of Coq-level variables.Use lazymatch in iClear to avoid backtracking on errors.Rename the internal validity uPred_valid into uPred_cmra_valid.Consistent syntax for generalization in iLöb and iInduction.CMRA structure on uPred.Relate map_to_list to nil.Relate "elements" of a finite set to nil.Alternative version of ownM_empty.Insert and singleton maps are non-empty.Binary mononicity property for CMRA op.Reorganize frame preserving updates for lists.More properties for the list CMRA.More derived auth properties.Mononicity of own.Lemma for inclusion of excl similar to dec_agree.Setoid injectivity of Some.Lemma for inclusion of dec_agree.Lemma for inclusion of singleton gmaps.Validity lemmas for deletion in gmaps.Destructors for csum.Make it possible to frame hypotheses using specialization patterns.Make iFrame finish the goal if everything has been framed.Better representation of specialization patterns.Validity and update lemmas for owning multiple ghosts.Use ⊆ type class for set-like inclusion of lists.Make iSplit{L,R} ignore persistent hypotheses.Define shorthand EqDecision A := (∀ x y : A, Decision (x = y)).Document iInduction.Attempt at an iInduction tactic.New iFresh' H tactic that generates names starting with H.Better implementation of iLöb.Support for framing pure hypotheses.Definition of FromPure that is symmetric w.r.t. IntoPure.Better error message for iTimeless.Also change the core of coPset to be the identity.Merge branch 'master' into 'master' [from_exist_later] for instantiating an existential behind a later.Change hypotheses order for [frame_later] for better perfs.Make iFrame able to strip a later from a framed hypothesis when framing under a later.Make Is_true a typeclass.