Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa protected
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.023Jun21161312928Apr252019141110654130Mar29272423171615131042128Feb272221201428Jan2011Nov109828Sep207129Aug25181084128Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26remove unused importimprove commentstreamline definition of priority inversionrefactor interference definitionsRemove task_interference_received_before_decRemove redundant hypothesisUse valid_arrival_sequenceCleanupbump Coq and mathcomp versionsmake abstract quiet time boolSilence a non-uniform coercion warningclean up priority-related factsclean up some FIFO facts`always_higher_priority` is trivial for JLFP policiesadd hints to avoid busy-window `destruct`-ingprotect TODO comments from spell checkerprepare_MC_PRprepare_MC_PRAdd MathComp to wordlistMathComp PR TODO for sum_majorant_eqnMathComp PR TODO for sumnB_natMathComp PR TODO for leq_sum_seq_predMathComp PR TODO for {l,}eq_sum_seqMathComp PR TODO for leq_sum_sub_uniqMathComp PR TODO for sum_nat_eq0_natMathComp PR TODO for leq_subRL_implMathComp PR TODO for subdnDMathComp PR TODO for sum_nat_gt0Revert "reorganize `util.sum` and add some comments"fix overlooked deprecation warningsrewrite proof to fix unused-intro-pattern warningsilence one redundant canonical projection warningdisable ambiguous-paths warningsupdate mailmapadd RTA for ELF assuming bounded PIIntegrate rt_eauto into done (hence by and //)update guidelinesAmend FP bounded_nps to use generalised JLFP PI lemmaschange POET's task notationweaken one assumptionadd some helper lemmasCI: switch to custom mathcomp image