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

Default Goal Selector does not work that way on Coq 8.8

parent 233bed09
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
theories/options.v
+ 2
− 1
View file @ e88e601f
...@@ -6,7 +6,8 @@ but not transitively. *) ...@@ -6,7 +6,8 @@ but not transitively. *)
Export Set Default Proof Using "Type". Export Set Default Proof Using "Type".
(* FIXME: cannot enable this yet as some files disable 'Default Proof Using'. (* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
Export Set Suggest 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 (* "Fake" import to whitelist this file for the check that ensures we import
this file everywhere. this file everywhere.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment