Skip to content
Snippets Groups Projects
Commit adb9363c authored by Ralf Jung's avatar Ralf Jung
Browse files

also Set Default Goal Selector

parent 37e03ceb
No related branches found
No related tags found
1 merge request!185Add "options" file
......@@ -4,6 +4,9 @@ file is *imported*, the option will only apply on the import site
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 "!".
(* "Fake" import to whitelist this file for the check that ensures we import
this file everywhere.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment