From 0157aadd967fcba870fb9bf74ea2af7671105efc Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 19 Mar 2008 18:46:59 +0000
Subject: Coq.Relations.Relations can move back to its short name

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

(limited to 'theories/Sorting')

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index b75aee610..2d639d096 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -12,7 +12,7 @@
 
 (* G. Huet 1-9-95 uses Multiset *)
 
-Require Import List Multiset Permutation Coq.Relations.Relations Sorting.
+Require Import List Multiset Permutation Relations Sorting.
 
 Section defs.
 
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 97e4b02cc..f7bd37ee2 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Omega Coq.Relations.Relations Setoid List Multiset Permutation.
+Require Import Omega Relations Setoid List Multiset Permutation.
 
 Set Implicit Arguments.
 
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index f0b849b6c..814ef0408 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Omega Coq.Relations.Relations Multiset Permutation SetoidList.
+Require Import Omega Relations Multiset Permutation SetoidList.
 
 Set Implicit Arguments.
 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index ee8c192a6..e9bbf88e3 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Coq.Relations.Relations List Multiset Arith.
+Require Import 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 8fed110fe..4c8173172 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import List Multiset Permutation Coq.Relations.Relations.
+Require Import List Multiset Permutation Relations.
 
 Set Implicit Arguments.
 
-- 
cgit v1.2.3