aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/fingraph.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/ssreflect/fingraph.v')
-rw-r--r--mathcomp/ssreflect/fingraph.v5
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 1a0f25f..42346e2 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -1,8 +1,7 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path fintype.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
+From mathcomp Require Import seq path fintype.
(******************************************************************************)
(* This file develops the theory of finite graphs represented by an "edge" *)