From 4e04399adcf1a1efafc6be273ef7a436ed10cbf1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 19 Nov 2019 23:58:04 +0100
Subject: [PATCH] disambiguate Require commands in rt.util and rt.classic.util

---
 classic/util/bigcat.v        | 2 +-
 classic/util/counting.v      | 2 +-
 classic/util/div_mod.v       | 2 +-
 classic/util/list.v          | 2 +-
 classic/util/nat.v           | 2 +-
 classic/util/notation.v      | 2 +-
 classic/util/seqset.v        | 2 +-
 classic/util/step_function.v | 2 +-
 classic/util/sum.v           | 8 ++++++--
 classic/util/tactics.v       | 2 +-
 util/nondecreasing.v         | 6 +++++-
 util/search_arg.v            | 2 +-
 util/sum.v                   | 6 +++++-
 13 files changed, 26 insertions(+), 14 deletions(-)

diff --git a/classic/util/bigcat.v b/classic/util/bigcat.v
index 28051b5..d4ecebc 100644
--- a/classic/util/bigcat.v
+++ b/classic/util/bigcat.v
@@ -1,4 +1,4 @@
-From rt.util Require Export bigcat.
+Require Export rt.util.bigcat.
 
 Require Import rt.classic.util.tactics rt.classic.util.notation rt.classic.util.bigord.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/classic/util/counting.v b/classic/util/counting.v
index d581958..a1710fc 100644
--- a/classic/util/counting.v
+++ b/classic/util/counting.v
@@ -1,4 +1,4 @@
-From rt.util Require Export counting.
+Require Export rt.util.counting.
 
 Require Import rt.classic.util.tactics rt.classic.util.ord_quantifier.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/classic/util/div_mod.v b/classic/util/div_mod.v
index 40f2199..3097632 100644
--- a/classic/util/div_mod.v
+++ b/classic/util/div_mod.v
@@ -1,4 +1,4 @@
-From rt.util Require Export div_mod.
+Require Export rt.util.div_mod.
 
 Require Import Arith Omega Nat.
 Require Import rt.classic.util.tactics rt.util.ssromega rt.classic.util.nat.
diff --git a/classic/util/list.v b/classic/util/list.v
index b8d7d06..224fda9 100644
--- a/classic/util/list.v
+++ b/classic/util/list.v
@@ -1,4 +1,4 @@
-From rt.util Require Export list.
+Require Export rt.util.list.
 
 Require Import rt.classic.util.tactics.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/classic/util/nat.v b/classic/util/nat.v
index 8359327..e12a2c2 100644
--- a/classic/util/nat.v
+++ b/classic/util/nat.v
@@ -1,4 +1,4 @@
-From rt.util Require Export nat.
+Require Export rt.util.nat.
 
 Require Import rt.classic.util.tactics rt.util.ssromega.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
diff --git a/classic/util/notation.v b/classic/util/notation.v
index f0e803d..eacc5be 100644
--- a/classic/util/notation.v
+++ b/classic/util/notation.v
@@ -1,4 +1,4 @@
-From rt.util Require Export notation.
+Require Export rt.util.notation.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/util/seqset.v b/classic/util/seqset.v
index e1f3e36..648f03c 100644
--- a/classic/util/seqset.v
+++ b/classic/util/seqset.v
@@ -1,4 +1,4 @@
-From rt.util Require Export seqset.
+Require Export rt.util.seqset.
 
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype.
 
diff --git a/classic/util/step_function.v b/classic/util/step_function.v
index 9cbfd3e..447e03b 100644
--- a/classic/util/step_function.v
+++ b/classic/util/step_function.v
@@ -1,4 +1,4 @@
-From rt.util Require Export step_function.
+Require Export rt.util.step_function.
 
 Require Import rt.classic.util.tactics rt.classic.util.notation rt.classic.util.induction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
diff --git a/classic/util/sum.v b/classic/util/sum.v
index 6ed29ca..149025e 100644
--- a/classic/util/sum.v
+++ b/classic/util/sum.v
@@ -1,6 +1,10 @@
-From rt.util Require Export sum ssromega.
+Require Export rt.util.sum.
+Require Export rt.util.ssromega.
 
-From rt.classic.util Require Import tactics notation sorting nat.
+Require Import rt.classic.util.tactics.
+Require Import rt.classic.util.notation.
+Require Import rt.classic.util.sorting.
+Require Import rt.classic.util.nat.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 (* Lemmas about sum. *)
diff --git a/classic/util/tactics.v b/classic/util/tactics.v
index ed5a0e6..43182e4 100644
--- a/classic/util/tactics.v
+++ b/classic/util/tactics.v
@@ -1,4 +1,4 @@
-From rt.util Require Export tactics.
+Require Export rt.util.tactics.
 
 (* *********************************************************************)
 (*                                                                     *)
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 9f272f6..9dde5da 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -1,4 +1,8 @@
-From rt.util Require Import epsilon nat list tactics ssromega.
+Require Import rt.util.epsilon.
+Require Import rt.util.nat.
+Require Import rt.util.list.
+Require Import rt.util.tactics.
+Require Import rt.util.ssromega.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Non-Decreasing Sequence and Distances *)
diff --git a/util/search_arg.v b/util/search_arg.v
index 33e70b5..555c06d 100644
--- a/util/search_arg.v
+++ b/util/search_arg.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
-From rt.util Require Import tactics.
+Require Import rt.util.tactics.
 
 (** This file introduces a function called search_arg that allows finding the
     argument within a given range for which a function is minimal w.r.t. to a
diff --git a/util/sum.v b/util/sum.v
index d34d20e..6bde1f6 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,4 +1,8 @@
-From rt.util Require Import tactics notation nat ssromega. 
+Require Import rt.util.tactics.
+Require Import rt.util.notation.
+Require Import rt.util.nat.
+Require Import rt.util.ssromega.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 (* Lemmas about sum. *)
-- 
GitLab