From 744e7f6a319f4d459a3cc2309f575d43041d75aa Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 16 Oct 2006 17:11:44 +0000
Subject: affichage des ... dans les scripts

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

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2d98891167..d49163bfba 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2190,7 +2190,8 @@ let hide_interp t ot gl =
   let t = eval_tactic te in
   match ot with 
   | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl
-  | Some t' -> abstract_tactic_expr (TacArg (Tacexp te)) (tclTHEN t t') gl
+  | Some t' ->
+      abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl
 
 (***************************************************************************)
 (* Substitution at module closing time *)
-- 
cgit v1.2.3