From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 28 Sep 2015 11:04:59 +0200
Subject: Make -load-vernac-object respect the loadpath.

This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.

This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
---
 CHANGES | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 950f2fab18..16d86c8ff1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,8 +54,9 @@ Tools
 - The -compile command-line option now takes the full path of the considered
   file, including the ".v" extension, and outputs a warning if such an extension
   is lacking.
-- The -require command-line option now takes a logical path of a given library
-  rather than a physical path.
+- The -require and -load-vernac-object command-line options now take a logical
+  path of a given library rather than a physical path, thus they behave like
+  Require [Import] path.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
-- 
cgit v1.2.3