diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 1c146e205..0ef4e0dcf 100644 --- 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 index 558771233..39623521b 100644 --- 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.