remove company-coq-local-symbols

- they are redundant with `.dir-locals.el` - there are still a few symbols defined in `lebesgue_integral.v` but they might disappear with an anticipated change of ASCII notation
math-comp · May 17, 2022 · bfa6d4b · bfa6d4b
1 parent 039fc52
commit bfa6d4b
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 2 deletions.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -1,4 +1,3 @@
-(* -*- company-coq-local-symbols: (("`&`" . ?∩) ("`|`" . ?∪) ("set0" . ?∅)); -*- *)
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.

diff --git a/theories/set_interval.v b/theories/set_interval.v
@@ -1,4 +1,3 @@
-(* -*- company-coq-local-symbols: (("`&`" . ?∩) ("`|`" . ?∪) ("set0" . ?∅)); -*- *)
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.