diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-26 15:12:42 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-26 15:12:42 +0000 |
| commit | fd3692cdc85049cce6fa7923c90e2b60c1627b48 (patch) | |
| tree | 3a477eb0d6110db0207235ab917251e5d51d24ce | |
| parent | 2e7eb4d3049b3d26d1efbe3843a68c63f8a21648 (diff) | |
closed bug 1898: fold x in x; added a reordering primitive tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11633 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/printer.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 63accefd1..bfb571b23 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -474,6 +474,9 @@ let pr_prim_rule = function (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) + | Order ord -> + (str"order " ++ prlist_with_sep pr_spc pr_id ord) + | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) |