diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-04 21:09:46 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-04 21:09:46 +0100 |
| commit | e59eeb6f0d8c8bcee12d97c6be6c1b972ba36cd5 (patch) | |
| tree | dbed2df57edd4456875e187e1de32862472aa9be /proofs/logic.ml | |
| parent | 62d366647146650d760b685b88d6ee4295e4a55b (diff) | |
Removing the old rename tactic.
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 13 |
1 files changed, 0 insertions, 13 deletions
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) |