diff options
| -rw-r--r-- | printing/printer.ml | 4 | ||||
| -rw-r--r-- | proofs/logic.ml | 13 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 7 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
6 files changed, 0 insertions, 27 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 1880d90ee..5b88e8c98 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -697,10 +697,6 @@ let pr_prim_rule = function (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) - | Rename (id1,id2) -> - (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) - - (* Backwards compatibility *) let prterm = pr_lconstr diff --git a/proofs/logic.ml b/proofs/logic.ml index 3be202476..aa99dd036 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -673,16 +673,3 @@ let prim_refiner r sigma goal = let (gl,ev,sigma) = mk_goal hyps' cl in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) - - | Rename (id1,id2) -> - if !check && not (Id.equal id1 id2) && - Id.List.mem id2 - (ids_of_named_context (named_context_of_val sign)) - then - error ((Id.to_string id2)^" is already used."); - let sign' = rename_hyp id1 id2 sign in - let cl' = replace_vars [id1,mkVar id2] cl in - let (gl,ev,sigma) = mk_goal sign' cl' in - let ev = Vars.replace_vars [(id2,mkVar id1)] ev in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in - ([gl], sigma) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 925aff10e..d7e1c7b53 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -34,7 +34,6 @@ type prim_rule = | Refine of constr | Thin of Id.t list | Move of bool * Id.t * Id.t move_location - | Rename of Id.t * Id.t (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 1fb73b7ad..2225a6e30 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -26,7 +26,6 @@ type prim_rule = | Refine of constr | Thin of Id.t list | Move of bool * Id.t * Id.t move_location - | Rename of Id.t * Id.t (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7349a8273..5b3605224 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 *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3ee970c1f..a9f7bffbf 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -100,7 +100,6 @@ val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic val thin : Id.t list -> tactic val move_hyp : bool -> Id.t -> Id.t move_location -> tactic -val rename_hyp : (Id.t*Id.t) list -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds |