From 8e25e107a8715728a7227934d7b11035863ee5f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 25 Sep 2015 12:25:35 +0200
Subject: The -require option now accepts a logical path instead of a physical
 one.

---
 man/coqide.1 | 10 +++++-----
 man/coqtop.1 |  8 ++++----
 2 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'man')

diff --git a/man/coqide.1 b/man/coqide.1
index 3fa7f0e41..cfd9c3b4a 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -67,11 +67,11 @@ Load Coq file
 Load Coq object file
 .IR f .vo.
 .TP
-.BI \-require\  f
-Load Coq object file
-.IR f .vo
-and import it (Require
-.IR f .).
+.BI \-require\  path
+Load Coq library
+.IR path
+and import it (Require Import
+.IR path .).
 .TP
 .BI \-compile\  f
 Compile Coq file
diff --git a/man/coqtop.1 b/man/coqtop.1
index 705ea43f6..e079bee39 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -78,10 +78,10 @@ load Coq object file
 .I filename.vo
 
 .TP
-.BI \-require \ filename
-load Coq object file
-.I filename.vo
-and import it (Require Import filename.)
+.BI \-require \ path
+load Coq library
+.I path
+and import it (Require Import path.)
 
 .TP
 .BI \-compile \ filename.v
-- 
cgit v1.2.3