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.021Jun201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211get rid of to_val_is_Some'print whether we are testing or creating reference outputchange the way we generate test reference filesuse lia instead of omegaattempt to fix tests timingimplement proper dependency tracking for test filesMerge branch 'master' into gen_proofmodebackport heap_lang notation fix from gen_proofmodeMerge branch 'ralf/into_val' into 'gen_proofmode'change AsVal to be easier to use (like IntoVal)change IntoVal so that it is easier to use in specsmake coercions explicit to improve readabilitytest against Coq 8.8 development branchcomment for how we plan to generalize the WP notation if necessaryremove Pos.succ from proofmode unfold list by making a copyimprove and test iApply error messageMerge branch 'ralf/errors' into 'gen_proofmode'Merge branch 'robbert/big_sepL2' into 'gen_proofmode'Tests for `big_sepL2`.test and fix some more proof mode error messagesMake Ltac helper function localProof mode error messages: Print hypothesis name without [INamed]Proof mode class instances for `big_sepL2`.Separating big operator over two lists.Adding `%I` to printing of proof mode hypotheses.Use `IsCons` and `IsApp` more consistently.Move comment about `IsCons` and `IsApp`.More ▷ commute lemmas for big operators.Add missing Import.Merge branch 'ralf/pm_red' into 'gen_proofmode'Merge branch 'ci/robbert/overloaded_wp' into 'gen_proofmode'move the reduction control of the proofmode to its own file and tweak itTypeclass to overload WP notation.attempt to fix reftests for older versions of CoqMerge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodedocument WP format stringsMerge branch 'ralf/reftests' into 'gen_proofmode'also test the output of error messagesMove local recursive ltac functions out to their own definitions to shorten backtracesbump stdpp