aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-11-09 21:04:56 +0100
committerPierre-Marie Pédrot2014-11-09 21:04:56 +0100
commit2070c302639e841aae1558e8bc59cca6da099bdd (patch)
tree991c54cf03e8e380714308a3ec154137b6cd7de4 /printing
parent90c398a7377ac4dbab5ed3add3cbbe9a1bea538a (diff)
Removing a unused boolean in the TacMove node of tacexpr AST.
Diffstat (limited to 'printing')
-rw-r--r--printing/pptactic.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 44f4b456cc..9c9bba45b7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -879,9 +879,7 @@ module Make
keyword "clearbody" ++ spc ()
++ prlist_with_sep spc pr.pr_name l
)
- | TacMove (b,id1,id2) ->
- (* Rem: only b = true is available for users *)
- assert b;
+ | TacMove (id1,id2) ->
hov 1 (
keyword "move"
++ brk (1,1) ++ pr.pr_name id1