Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5
  • v0.4
  • v0.3
  • v0.2
  • v0.1
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.019Nov181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug26252418171211654331Jul30292827252422211716151413121110987611Jun15May8765430Apr22212023Mar658Aug131Jul3029Add lemma about arrivals in empty intervalMove workload lemma to basic filesAdd file to util.allAdd lemma to util.sumAdd lemmas to util.listAdd tactics for inequalitiesImprove documentation in restructuring/behaviorUpdate coqdocjsdocument the --only-classic optioncleanup create_makefile.shcreate_makefile.sh: add --only-classic optionmention classic/util in READMEmove unused helper lemmas/notations/tactics to rt.classicdo not rely on simpl_sum_const tacticdo not use vlib 'edone' when plain 'eassumption' will dodo not rely on vlib 'des' tacticdo not rely on vlib x <= y <= z auto-splittingDon't re-generate _CoqProject in create_makefile.shcreate_makefile.sh: support --without-classicproofloc.py: do not count proofs that have been commented outproofloc.py: fix single-line proof patternadd READMEs to behavior and model modulesupdate explanation of new Prosa's structuredocument additional guidelinesupdate documentation and guidelinesUpdate top-level and classic/ READMEsupdate paths in the known long proofs databaseupdate Require'd module names to rt.classic namespacemove classic Prosa into rt.classic namespaceupdate mathcomp documentation URLminor fix: remove erroneous coqdoc formatting syntaxMake cores explicit in ProcessorStatemake a few cosmetic tweaks in the EDF optimality proofmake the proof term in the readiness type class "unreferencable"add CI job for testing against latest ssreflectmake processor state explicit in platform propertiesconvert comments in behavior modulefix links to Coq standard library in coqdoc outputconvert comments in analysis moduleupdate create_makefile.sh to patch up coqdoc.css