diff options
| author | Pierre-Marie Pédrot | 2014-11-04 21:09:46 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-04 21:09:46 +0100 |
| commit | e59eeb6f0d8c8bcee12d97c6be6c1b972ba36cd5 (patch) | |
| tree | dbed2df57edd4456875e187e1de32862472aa9be /proofs/tacmach.ml | |
| parent | 62d366647146650d760b685b88d6ee4295e4a55b (diff) | |
Removing the old rename tactic.
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7349a82730..5b36052244 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -125,12 +125,6 @@ let thin_no_check ids gl = let move_hyp_no_check with_dep id1 id2 gl = refiner (Move (with_dep,id1,id2)) gl -let rec rename_hyp_no_check l gl = match l with - | [] -> tclIDTAC gl - | (id1,id2)::l -> - tclTHEN (refiner (Rename (id1,id2))) - (rename_hyp_no_check l) gl - let mutual_fix f n others j gl = with_check (refiner (FixRule (f,n,others,j))) gl @@ -145,7 +139,6 @@ let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) let thin c = with_check (thin_no_check c) let move_hyp b id id' = with_check (move_hyp_no_check b id id') -let rename_hyp l = with_check (rename_hyp_no_check l) (* Pretty-printers *) |