From 493c49eb5db77128ca6d09177f557ed98cb0ee0e Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 30 May 2024 07:49:47 +0200 Subject: [PATCH] attempt to fix CI --- theories/lspace.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 22fc30a78..623ea6dad 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -79,10 +79,10 @@ Canonical Lequiv_canonical := Local Open Scope quotient_scope. Definition LspaceType := {eq_quot Lequiv}. -Canonical LspaceType_quotType := [quotType of LspaceType]. -Canonical LspaceType_eqType := [eqType of LspaceType]. -Canonical LspaceType_choiceType := [choiceType of LspaceType]. -Canonical LspaceType_eqQuotType := [eqQuotType Lequiv of LspaceType]. +Canonical LspaceType_quotType := [the quotType _ of LspaceType]. +Canonical LspaceType_eqType := [the eqType of LspaceType]. +Canonical LspaceType_choiceType := [the choiceType of LspaceType]. +Canonical LspaceType_eqQuotType := [the eqQuotType Lequiv of LspaceType]. Lemma LequivP (f g : LfunType mu p) : reflect {ae mu, forall x, f x = g x} (f == g %[mod LspaceType]).