From 791f3254cba602672b834ec3484d308db074b684 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Tue, 14 Jun 2016 15:58:36 +0200
Subject: Add documentation for goal selectors.

---
 proofs/proof_global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index be353b10ae..61fe347504 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -678,7 +678,7 @@ let print_goal_selector = function
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
   | i ->
-      let err_msg = "A selector must be \"all\" or a natural number." in
+      let err_msg = "The default selector must be \"all\" or a natural number." in
       begin try
               let i = int_of_string i in
               if i < 0 then Errors.error err_msg;
-- 
cgit v1.2.3