From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 proofs/tacmach.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'proofs/tacmach.ml')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6bbaff08..bf194d47 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: tacmach.ml 11639 2008-11-27 17:48:32Z barras $ *)
 
 open Pp
 open Util
@@ -202,6 +202,9 @@ let thin_body_no_check ids gl =
 let move_hyp_no_check with_dep id1 id2 gl = 
   refiner (Prim (Move (with_dep,id1,id2))) gl
 
+let order_hyps idl gl =
+  refiner (Prim (Order idl)) gl
+
 let rec rename_hyp_no_check l gl = match l with 
   | [] -> tclIDTAC gl 
   | (id1,id2)::l -> 
-- 
cgit v1.2.3