aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-05-03 00:38:25 +0200
committerPierre-Marie Pédrot2019-05-11 12:43:22 +0200
commitec6c11c67a01122f52f615691f120bde9da9a61e (patch)
tree16bcbe751040f6b87ca1b2b5679e9eabab63125d /dev/include
parent3c6ed7485293c7eb80f9c4d415af0ee0b977f157 (diff)
Introducing a local flag to hypothesis conversion function.
If the reduction function is known not to depend on the named context, then we can perform it in parallel on the various variables.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions