From 4560295f90ab9d5c7cbb5718670c5067c732f42b Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 11 Sep 2024 17:03:05 +0200 Subject: [PATCH] adapt to MC#1258 --- theories/complex.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/theories/complex.v b/theories/complex.v index 6d3e96a..8b9ec83 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -1,10 +1,11 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From HB Require Import structures. -From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. -From mathcomp Require Import choice fintype tuple bigop binomial order ssralg. -From mathcomp Require Import zmodp poly ssrnum ssrint archimedean rat matrix. -From mathcomp Require Import mxalgebra mxpoly closed_field polyrcf realalg. +From mathcomp Require Import ssreflect ssrfun ssrbool ssrnotations eqtype. +From mathcomp Require Import ssrnat seq div choice fintype tuple bigop binomial. +From mathcomp Require Import order ssralg zmodp poly ssrnum ssrint archimedean. +From mathcomp Require Import rat matrix mxalgebra mxpoly closed_field polyrcf. +From mathcomp Require Import realalg. (**********************************************************************) (* This files defines the extension R[i] of a real field R, *) @@ -361,7 +362,7 @@ HB.export ComplexField. (* indeed, this would prevent C fril having a normed module over C *) Definition conjc {R : ringType} (x : R[i]) := let: a +i* b := x in a -i* b. -Notation "x ^*" := (conjc x) (at level 2, format "x ^*") : complex_scope. +Notation "x ^*" := (conjc x) : complex_scope. Local Open Scope complex_scope. Delimit Scope complex_scope with C.