diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 9 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 |
3 files changed, 9 insertions, 6 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index c78e842ec..8c45d95b3 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -166,7 +166,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacClear of bool * 'id list | TacClearBody of 'id list | TacMove of bool * 'id * 'id - | TacRename of 'id * 'id + | TacRename of ('id *'id) list (* Constructors *) | TacLeft of 'constr bindings diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2049eb0f6..68cd19479 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -205,8 +205,11 @@ 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 rename_hyp_no_check id1 id2 gl = - refiner (Prim (Rename (id1,id2))) gl +let rec rename_hyp_no_check l gl = match l with + | [] -> tclIDTAC gl + | (id1,id2)::l -> + tclTHEN (refiner (Prim (Rename (id1,id2)))) + (rename_hyp_no_check l) gl let mutual_fix f n others gl = with_check (refiner (Prim (FixRule (f,n,others)))) gl @@ -234,7 +237,7 @@ let convert_hyp d = with_check (convert_hyp_no_check d) let thin l = with_check (thin_no_check l) let thin_body c = with_check (thin_body_no_check c) let move_hyp b id id' = with_check (move_hyp_no_check b id id') -let rename_hyp id id' = with_check (rename_hyp_no_check id id') +let rename_hyp l = with_check (rename_hyp_no_check l) (* Pretty-printers *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 817f934db..1d0cfe0d6 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -132,7 +132,7 @@ val convert_hyp_no_check : named_declaration -> tactic val thin_no_check : identifier list -> tactic val thin_body_no_check : identifier list -> tactic val move_hyp_no_check : bool -> identifier -> identifier -> tactic -val rename_hyp_no_check : identifier -> identifier -> tactic +val rename_hyp_no_check : (identifier*identifier) list -> tactic val mutual_fix : identifier -> int -> (identifier * int * constr) list -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> tactic @@ -150,7 +150,7 @@ val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val thin_body : identifier list -> tactic val move_hyp : bool -> identifier -> identifier -> tactic -val rename_hyp : identifier -> identifier -> tactic +val rename_hyp : (identifier*identifier) list -> tactic (*s Tactics handling a list of goals. *) |