From 125f04f251e62674379dfe9ae7ee660586e5c954 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 14 Mar 2008 20:27:40 +0000
Subject: Suppress some warnings by writing ugly Coq.Relations.Relations in
 some .v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10672 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Sorting/Heap.v         | 7 +------
 theories/Sorting/PermutEq.v     | 7 +------
 theories/Sorting/PermutSetoid.v | 7 +------
 theories/Sorting/Permutation.v  | 5 +----
 theories/Sorting/Sorting.v      | 5 +----
 5 files changed, 5 insertions(+), 26 deletions(-)

(limited to 'theories/Sorting')

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 573d5adb8..b75aee610 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -12,12 +12,7 @@
 
 (* G. Huet 1-9-95 uses Multiset *)
 
-Require Import List.
-Require Import Multiset.
-Require Import Permutation.
-Require Import Relations.
-Require Import Sorting.
-
+Require Import List Multiset Permutation Coq.Relations.Relations Sorting.
 
 Section defs.
 
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 8ff4e460e..97e4b02cc 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -8,12 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Omega.
-Require Import Relations.
-Require Import Setoid.
-Require Import List.
-Require Import Multiset.
-Require Import Permutation. 
+Require Import Omega Coq.Relations.Relations Setoid List Multiset Permutation.
 
 Set Implicit Arguments.
 
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index e012bde19..f0b849b6c 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -8,12 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Omega.
-Require Import Relations.
-Require Import List.
-Require Import Multiset.
-Require Import Permutation. 
-Require Import SetoidList.
+Require Import Omega Coq.Relations.Relations Multiset Permutation SetoidList.
 
 Set Implicit Arguments.
 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 2f8ef8d11..ee8c192a6 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -8,10 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Coq.Relations.Relations.
-Require Import List.
-Require Import Multiset.
-Require Import Arith.
+Require Import Coq.Relations.Relations List Multiset Arith.
 
 (** This file define a notion of permutation for lists, based on multisets: 
     there exists a permutation between two lists iff every elements have 
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 9828d1a24..8fed110fe 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -8,10 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import List.
-Require Import Multiset.
-Require Import Permutation.
-Require Import Relations.
+Require Import List Multiset Permutation Coq.Relations.Relations.
 
 Set Implicit Arguments.
 
-- 
cgit v1.2.3