From 7057e7e9ab1160fc0e176182b6e71f720784715a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 4 Sep 2014 19:08:45 +0200 Subject: Revert the two previous commits. I was testing in the wrong branch. --- plugins/decl_mode/decl_proof_instr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b5566127f..8f20cea6b 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)) - (Proofview.V82.of_tactic (clear_body [id])) gls in + (thin_body [id]) gls in tclMAP add_aux items gls let prepare_goal items gls = -- cgit v1.2.3