From e4dd5d40cf0da9b0b692274508da244ba4288f5a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Dec 2000 15:24:56 +0000
Subject: Amélioration message d'erreur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1106 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fd58ae3ed5..c194917721 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1583,10 +1583,12 @@ let _ =
 	 |  _  -> invalid_arg "SOLVE"
        in
        (fun () -> 
+	  if not (refining ()) then
+	    error "Unknown command of the non proof-editing mode";
 	  solve_nth n (Tacinterp.interp tcom);
 	  print_subgoals();
           (* in case a strict subtree was completed, 
-              go back to the top of the prooftree *) 
+             go back to the top of the prooftree *) 
 	  if subtree_solved () then 
 	    (reset_top_of_tree (); print_subgoals()) 
        ))
-- 
cgit v1.2.3