diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index c4b7ad13c0..133524ba76 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Util open Pp @@ -261,7 +261,8 @@ let add_justification_hyps keep items gls = | _ -> let id=pf_get_new_id local_hyp_prefix gls in keep:=Idset.add id !keep; - letin_tac false (Names.Name id) c Tacexpr.nowhere gls in + tclTHEN (letin_tac None (Names.Name id) c Tacexpr.nowhere) + (thin_body [id]) gls in tclMAP add_aux items gls let prepare_goal items gls = @@ -807,7 +808,7 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac true (Name id) t Tacexpr.nowhere gls + letin_tac None (Name id) t Tacexpr.nowhere gls (* tactics for reconsider *) |