From 8af881ff3950284b33b19a5535641e1b3a698b4d Mon Sep 17 00:00:00 2001
From: delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 21 Nov 2000 22:29:40 +0000
Subject: Elimination d'un test sur les macros

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e33c9655a..53d0c7b51 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1526,16 +1526,6 @@ let _ =
 	 |  _  -> invalid_arg "SOLVE"
        in
        (fun () -> 
-	  (match Tacinterp.is_just_undef_macro tcom with
-             | Some id -> 
-		 let msg =
- 	     	   if Pfedit.refining () then 
-		     "undefined command or tactic"
-	     	   else 
-		     "undefined command"
-		 in 
-		 error msg
-	     | None -> ());
 	  solve_nth n (Tacinterp.interp tcom);
 	  print_subgoals();
           (* in case a strict subtree was completed, 
-- 
cgit v1.2.3