From f7e0b60554789d3859562ae533961bb04fc4ec84 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 6 Jul 2007 15:31:37 +0000 Subject: extension of the rename tactic: the following is now allowed: rename A into B, C into D, E into F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tacinterp.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'tactics/tacinterp.ml') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d52093230..944b7710a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -717,8 +717,11 @@ let rec intern_atomic lf ist x = | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l) | TacMove (dep,id1,id2) -> TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2) - | TacRename (id1,id2) -> TacRename (intern_hyp_or_metaid ist id1, intern_hyp_or_metaid ist id2) - + | TacRename l -> + TacRename (List.map (fun (id1,id2) -> + intern_hyp_or_metaid ist id1, + intern_hyp_or_metaid ist id2) l) + (* Constructors *) | TacLeft bl -> TacLeft (intern_bindings ist bl) | TacRight bl -> TacRight (intern_bindings ist bl) @@ -2125,8 +2128,10 @@ and interp_atomic ist gl = function | TacClearBody l -> h_clear_body (interp_hyp_list ist gl l) | TacMove (dep,id1,id2) -> h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2) - | TacRename (id1,id2) -> - h_rename (interp_hyp ist gl id1) (interp_ident ist gl (snd id2)) + | TacRename l -> + h_rename (List.map (fun (id1,id2) -> + interp_hyp ist gl id1, + interp_ident ist gl (snd id2)) l) (* Constructors *) | TacLeft bl -> h_left (interp_bindings ist gl bl) @@ -2426,7 +2431,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacClear _ as x -> x | TacClearBody l as x -> x | TacMove (dep,id1,id2) as x -> x - | TacRename (id1,id2) as x -> x + | TacRename l as x -> x (* Constructors *) | TacLeft bl -> TacLeft (subst_bindings subst bl) -- cgit v1.2.3