diff options
| author | msozeau | 2008-09-02 19:34:23 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-02 19:34:23 +0000 |
| commit | 64f0c19dc57a4cba968115a9f8e9ffd128580fad (patch) | |
| tree | a70c1f9e41e39e88fa68feb9604c1e833ad5756d /parsing/pptactic.ml | |
| parent | 3a0b2a7d9188285d38a869a47a875ada66b9543c (diff) | |
- Remove some dead code in subtac
- Fix an apparent bug in the printing of move, indeed by default
move is _not_ dependent when parsed (see parsing/g_tactic.ml4).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11351 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 933667ce32..0eaac6a635 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -805,10 +805,9 @@ and pr_atom1 = function | TacClearBody l -> hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l) | TacMove (b,id1,id2) -> - (* Rem: only b = true is available for users *) - assert b; hov 1 - (str "move" ++ brk (1,1) ++ pr_ident id1 ++ + (str "move" ++ (if b then spc () ++ str"dependent" else mt ()) + ++ brk (1,1) ++ pr_ident id1 ++ pr_move_location pr_ident id2) | TacRename l -> hov 1 |