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.
---
 doc/refman/RefMan-com.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 0f1823a021..9862abb533 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -153,9 +153,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
   standard input.
 
-\item[{\tt -load-vernac-object} {\em file}]\ 
+\item[{\tt -load-vernac-object} {\em path}]\ 
 
-  Load \Coq~compiled file {\em file}{\tt .vo}
+  Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
 
 \item[{\tt -require} {\em path}]\ 
 
-- 
cgit v1.2.3