From f3ce9ace4b55654d6240db9eb41a6de3c488f0d9 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 6 Feb 2018 14:04:50 +0100 Subject: fixing things that @ggonthier and @ybertot spotted and some I spotted --- mathcomp/solvable/gfunctor.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/solvable/gfunctor.v') diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index 7fbee8c..fc8385d 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -158,7 +158,7 @@ End Definitions. Section ClassDefinitions. Structure iso_map := IsoMap { - apply: object_map; + apply : object_map; _ : group_valued apply; _ : closed apply; _ : iso_continuous apply -- cgit v1.2.3