diff options
| author | Pierre-Marie Pédrot | 2016-05-17 11:02:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 11:06:14 +0200 |
| commit | 43343c1f79d9f373104ae5174baf41e2257e2b8d (patch) | |
| tree | 7ac3a1ec228702fd8bf81c828e3d3e1c8f0ebc3c /plugins/decl_mode | |
| parent | cddddce068bc0482f62ffab8e412732a307b90bb (diff) | |
Removing the old refine tactic from the Tactics module.
It is indeed confusing, as it has little to do with the proper refine defined
in the New submodule. Legacy code relying on it should call the Logic or
Tacmach modules instead.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index de06af0053..be6ce59bd3 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -485,7 +485,7 @@ let thus_tac c ctyp submetas gls = Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in - Tactics.refine refiner gls + Tacmach.refine refiner gls (* general forward step *) |