diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-06 15:31:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-06 15:31:37 +0000 |
| commit | f7e0b60554789d3859562ae533961bb04fc4ec84 (patch) | |
| tree | 0d368092cbb361ecc13023fdbdd747e94765dc70 /proofs | |
| parent | 7d030bc502378e89d81947bac91820047bdd0380 (diff) | |
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
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. *) |