From c83609826d97afda6b11b227207f461cf077a0d5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 19 Nov 2020 19:18:39 +0900 Subject: add declare scopes --- mathcomp/fingroup/presentation.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'mathcomp/fingroup/presentation.v') diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v index af453aa..0137377 100644 --- a/mathcomp/fingroup/presentation.v +++ b/mathcomp/fingroup/presentation.v @@ -52,6 +52,9 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope group_presentation. +Declare Scope nt_group_presentation. + Import GroupScope. Module Presentation. -- cgit v1.2.3