aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2018-06-08 13:12:19 +0200
committerMatthieu Sozeau2018-09-06 16:43:38 +0200
commita488da64eb852554e0f1e60e2c94ea8cfc525dd7 (patch)
treee24903bd36134020a382b9b3d8ca9a956bd05448 /dev
parent51197c3b8b5a6f30397f0263e2e2f4461519c66e (diff)
Bound proof-search in default program obligation tactic.
This issue was first reported on equations where a definition seemingly took all memory until Coq crashed. https://github.com/mattam82/Coq-Equations/issues/69
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions