Skip to content
Snippets Groups Projects
Verified Commit 87095c3b authored by Tej Chajed's avatar Tej Chajed
Browse files

Remove global strict bulleting flag

parent 6b48804f
No related branches found
No related tags found
1 merge request!184Switch to strict bulleting everywhere
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 4 deletions
theories/base.v
+ 0
− 4
View file @ 87095c3b
...@@ -14,10 +14,6 @@ Set Default Proof Using "Type". ...@@ -14,10 +14,6 @@ Set Default Proof Using "Type".
Export ListNotations. Export ListNotations.
From Coq.Program Require Export Basics Syntax. From Coq.Program Require Export Basics Syntax.
(* TODO: remove this once it's set by an options file (the below command affects
all transitive users, which we don't want to do) *)
Global Set Default Goal Selector "!".
(** This notation is necessary to prevent [length] from being printed (** This notation is necessary to prevent [length] from being printed
as [strings.length] if strings.v is imported and later base.v. See as [strings.length] if strings.v is imported and later base.v. See
also strings.v and also strings.v and
......
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