diff options
| author | Pierre-Marie Pédrot | 2014-09-04 17:58:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 18:06:16 +0200 |
| commit | 6828b31acdf10cf7987f0e494f6f7505a15b1000 (patch) | |
| tree | 98497c88a99aaa7453b605c30957a28b4916937c /plugins | |
| parent | 99a70a4e2e19441f29667b243b232f5f9f1059a2 (diff) | |
Removing the old implementation of clear_body.
Diffstat (limited to 'plugins')
| -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 8f20cea6be..b5566127f1 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -222,7 +222,7 @@ let add_justification_hyps keep items gls = let id=pf_get_new_id local_hyp_prefix gls in keep:=Id.Set.add id !keep; tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere)) - (thin_body [id]) gls in + (Proofview.V82.of_tactic (clear_body [id])) gls in tclMAP add_aux items gls let prepare_goal items gls = |