aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-07 16:25:17 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-07 16:25:17 +0000
commitf2b1574af959529d2881189a91e0d39aea627dc1 (patch)
tree7d4cf87fdc8e86ef7fe3dd8ec72e602efd65d05f /toplevel
parentf493b6f2b103dd4e2d0b86acae2fcc7a2b76bdcf (diff)
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
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9c30cef9a..9e53e01c4 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 *)