search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
41 stars 24 forks source link

set Default Proof Using "All" in every Section #42

Closed andres-erbsen closed 3 years ago

andres-erbsen commented 3 years ago

Alternative to #39

andres-erbsen commented 3 years ago

@JasonGross I couldn't get _CoqProject arguments to work on master https://github.com/mit-plv/coqutil/runs/3637019029#step:5:38

JasonGross commented 3 years ago

@JasonGross I couldn't get _CoqProject arguments to work on master https://github.com/mit-plv/coqutil/runs/3637019029#step:5:38

Try -arg "Default\ Proof\ Using\ \"All\"" and if that doesn't work, try futzing with the quoting, like, maybe -arg 'Default Proof Using "All"'? If none of this works, report it as a usability bug in -set.