From f2b1574af959529d2881189a91e0d39aea627dc1 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 7 Feb 2001 16:25:17 +0000
Subject: Reparation du pretty-print pour les tactiques

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

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9c30cef9a6..9e53e01c4e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1732,7 +1732,7 @@ let _ =
        (fun () -> 
 	  if not (refining ()) then
 	    error "Unknown command of the non proof-editing mode";
-	  solve_nth n (Tacinterp.interp tcom);
+	  solve_nth n (Tacinterp.hide_interp tcom);
 	  print_subgoals();
           (* in case a strict subtree was completed, 
              go back to the top of the prooftree *) 
-- 
cgit v1.2.3