diff options
| author | letouzey | 2007-07-06 15:55:39 +0000 |
|---|---|---|
| committer | letouzey | 2007-07-06 15:55:39 +0000 |
| commit | 4d75ddfdc0382e0d6e163febe12912fe477aa43b (patch) | |
| tree | ed55e513dd72f6c57c246a147a66f7dc21bdd7f7 | |
| parent | f7e0b60554789d3859562ae533961bb04fc4ec84 (diff) | |
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
| -rw-r--r-- | contrib/interface/xlate.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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)) |