From fd3692cdc85049cce6fa7923c90e2b60c1627b48 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 26 Nov 2008 15:12:42 +0000
Subject: 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
---
 parsing/printer.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 63accefd11..bfb571b236 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)
 
-- 
cgit v1.2.3