Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • prepare_MC_PR
  • tutorial
  • classic-prosa protected
  • wip-hunspell
  • fset
  • embed_arr_seq_uniq
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
Blame Permalink
  • Sergey Bozhko's avatar
    e3567e95
    add lemmas about [service_of_jobs] · e3567e95
    Sergey Bozhko authored and Björn Brandenburg's avatar Björn Brandenburg committed 
    This commit also removes one spurious dependency on ideal uni-processor.
That is, previously file [model/service_of_jobs.v] imported
[processor.ideal], which is wrong, since [model/service_of_jobs.v]
assumes no specific model for processor.
    e3567e95
    History
    add lemmas about [service_of_jobs]
    Sergey Bozhko authored and Björn Brandenburg's avatar Björn Brandenburg committed 
    This commit also removes one spurious dependency on ideal uni-processor.
That is, previously file [model/service_of_jobs.v] imported
[processor.ideal], which is wrong, since [model/service_of_jobs.v]
assumes no specific model for processor.