From 4d75ddfdc0382e0d6e163febe12912fe477aa43b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 6 Jul 2007 15:55:39 +0000
Subject: sequel to commit 9952: forgot to adapt xlate to the new n-ary rename

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9953 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 202e58472e..068110d747 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1197,7 +1197,8 @@ and xlate_tac =
 	  CT_use_inversion (id, xlate_formula c,
 	    CT_id_list (List.map xlate_hyp idlist))
     | TacExtend (_,"omega", []) -> CT_omega
-    | TacRename (id1, id2) -> CT_rename(xlate_hyp id1, xlate_hyp id2)
+    | TacRename [id1, id2] -> CT_rename(xlate_hyp id1, xlate_hyp id2)
+    | TacRename _ -> xlate_error "TODO: add support for n-ary rename"
     | TacClearBody([]) -> assert false
     | TacClearBody(a::l) -> 
 	CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
-- 
cgit v1.2.3