From 4db32ffb3a157077be771f753ba8b5e4a8efc631 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Jun 2017 17:05:27 +0200
Subject: Improving documentation of tactic "move" (report #4561).

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index c329bdf4aa..6af1b2d837 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -253,7 +253,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
             else
 	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
 	        Miscprint.pr_move_location pr_id hto ++
-	        str (if toleft then ": it occurs in " else ": it depends on ")
+	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
           else
 	    (d::first, middle)
-- 
cgit v1.2.3