diff options
| author | barras | 2006-10-16 17:11:44 +0000 |
|---|---|---|
| committer | barras | 2006-10-16 17:11:44 +0000 |
| commit | 744e7f6a319f4d459a3cc2309f575d43041d75aa (patch) | |
| tree | f130166bae5b1c1aa39860e8e5a2e79bfa284296 /tactics | |
| parent | 8fe195799d9bf4eb0c84fad3e9a79b78e6e224ec (diff) | |
affichage des ... dans les scripts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 *) |