From 29a193a3028bad95776b625d10d70a6fa52725d0 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 29 Jul 2015 12:03:02 +0200
Subject: fix PF

---
 mathcomp/odd_order/PFsection1.v | 1 +
 mathcomp/odd_order/PFsection8.v | 1 +
 2 files changed, 2 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v
index 6864887..7c74766 100644
--- a/mathcomp/odd_order/PFsection1.v
+++ b/mathcomp/odd_order/PFsection1.v
@@ -13,6 +13,7 @@ From mathcomp
 Require Import vector falgebra fieldext ssrnum algC rat algnum galois.
 From mathcomp
 Require Import classfun character inertia integral_char vcharacter.
+From mathcomp
 Require ssrint.
 
 (******************************************************************************)
diff --git a/mathcomp/odd_order/PFsection8.v b/mathcomp/odd_order/PFsection8.v
index ee0c7cc..fd085f6 100644
--- a/mathcomp/odd_order/PFsection8.v
+++ b/mathcomp/odd_order/PFsection8.v
@@ -17,6 +17,7 @@ From mathcomp
 Require Import BGsection1 BGsection3 BGsection7 BGsection10.
 From mathcomp
 Require Import BGsection14 BGsection15 BGsection16.
+From mathcomp
 Require ssrnum.
 From mathcomp
 Require Import algC classfun character inertia vcharacter.
-- 
cgit v1.2.3