From 52dc407a449cee6937fe50d8d3b773c815a17ea2 Mon Sep 17 00:00:00 2001 From: Felipe Cerqueira <felipec@mpi-sws.org> Date: Tue, 12 Jul 2016 15:19:20 +0200 Subject: [PATCH] Remove LoadPath from util/all.v --- util/all.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/util/all.v b/util/all.v index 0bb353a09..42eb874b2 100644 --- a/util/all.v +++ b/util/all.v @@ -1,5 +1,3 @@ -Add LoadPath ".." as rt. - Require Export rt.util.tactics. Require Export rt.util.notation. Require Export rt.util.bigcat. @@ -15,4 +13,4 @@ Require Export rt.util.powerset. Require Export rt.util.sorting. Require Export rt.util.ssromega. Require Export rt.util.sum. -Require Export rt.util.seqset. \ No newline at end of file +Require Export rt.util.seqset. -- GitLab