diff options
| author | Pierre-Marie Pédrot | 2014-09-04 17:58:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-05 11:59:42 +0200 |
| commit | 466c25ea43149deedf50e0105a6d1e69db91c8fd (patch) | |
| tree | 98d76bc6449162524c713554d9ee76afc55f1de1 /plugins/decl_mode | |
| parent | 8c54bdeec740fb9edd80e28ce743418bf1276b90 (diff) | |
Removing the old implementation of clear_body.
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 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 = |