diff --git a/theories/options.v b/theories/options.v index 7e3856858e2a8b84e9f61b0034e0de133151aee5..c94b63dccfa6a69830312476090b40b948ebe1cb 100644 --- a/theories/options.v +++ b/theories/options.v @@ -6,7 +6,8 @@ but not transitively. *) Export Set Default Proof Using "Type". (* FIXME: cannot enable this yet as some files disable 'Default Proof Using'. Export Set Suggest Proof Using. *) -Export Set Default Goal Selector "!". +(* FIXME: cannot enable this on Coq 8.8. +Export Set Default Goal Selector "!". *) (* "Fake" import to whitelist this file for the check that ensures we import this file everywhere.