diff options
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 |