Mentions légales du service

Skip to content
Snippets Groups Projects
Select Git revision
0 results
Blame Permalink
Forked from The Rocq Prover / The Rocq Prover
Source project has a limited visibility.
  • Pierre-Marie Pédrot's avatar
    dd0ac117
    Extend the -async-proofs-tac-j option to accept the value 0. · dd0ac117
    Pierre-Marie Pédrot authored 
    When this option is passed the integer 0, it now replaces the par: selector
with an equivalent combinator that does not spawn any new process and behaves
as all: solve [tac] instead. This is different from when passed the integer 1,
which means that a process is still spawned although it doesn't parallelize
anything.
    dd0ac117
    History
    Extend the -async-proofs-tac-j option to accept the value 0.
    Pierre-Marie Pédrot authored 
    When this option is passed the integer 0, it now replaces the par: selector
with an equivalent combinator that does not spawn any new process and behaves
as all: solve [tac] instead. This is different from when passed the integer 1,
which means that a process is still spawned although it doesn't parallelize
anything.